:: Schemes
:: by Stanis\l aw T. Czuba
::
:: Received December 17, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

scheme :: SCHEMS_1:sch 1
Schemat0{ P₁[ set ] } :

ex a being set st P₁[a]

provided

A1: for a being set holds P₁[a]

proof end;

scheme :: SCHEMS_1:sch 2
Schemat3{ P₁[ set , set ] } :

for b being set ex a being set st P₁[a,b]

provided

A1: ex a being set st
for b being set holds P₁[a,b]

proof end;

scheme :: SCHEMS_1:sch 3
Schemat8{ P₁[ set ], P₂[ set ] } :

( ( for a being set holds P₁[a] ) implies for a being set holds P₂[a] )

provided

A1: for a being set st P₁[a] holds
P₂[a]

proof end;

scheme :: SCHEMS_1:sch 4
Schemat9{ P₁[ set ], P₂[ set ] } :

( ( for a being set holds P₁[a] ) iff for a being set holds P₂[a] )

provided

A1: for a being set holds
( P₁[a] iff P₂[a] )

proof end;

scheme :: SCHEMS_1:sch 5
Schemat17{ P₁[ set ], P₂[] } :

( ( for a being set holds P₁[a] ) implies P₂[] )

provided

A1: for a being set st P₁[a] holds
P₂[]

proof end;

scheme :: SCHEMS_1:sch 6
Schemat18a{ P₁[ set ], P₂[ set ] } :

ex a being set st
for b being set holds
( P₁[a] or P₂[b] )

provided

A1: ( ex a being set st P₁[a] or for b being set holds P₂[b] )

proof end;

scheme :: SCHEMS_1:sch 7
Schemat18b{ P₁[ set ], P₂[ set ] } :

( ex a being set st P₁[a] or for b being set holds P₂[b] )

provided

A1: ex a being set st
for b being set holds
( P₁[a] or P₂[b] )

proof end;

scheme :: SCHEMS_1:sch 8
Schemat20b{ P₁[ set ], P₂[ set ] } :

ex a being set st
for b being set holds
( P₁[a] or P₂[b] )

provided

A1: for b being set ex a being set st
( P₁[a] or P₂[b] )

proof end;

scheme :: SCHEMS_1:sch 9
Schemat22a{ P₁[ set ], P₂[ set ] } :

for b being set ex a being set st
( P₁[a] & P₂[b] )

provided

A1: ( ex a being set st P₁[a] & ( for b being set holds P₂[b] ) )

proof end;

scheme :: SCHEMS_1:sch 10
Schemat22b{ P₁[ set ], P₂[ set ] } :

( ex a being set st P₁[a] & ( for b being set holds P₂[b] ) )

provided

A1: for b being set ex a being set st
( P₁[a] & P₂[b] )

proof end;

scheme :: SCHEMS_1:sch 11
Schemat23b{ P₁[ set ], P₂[ set ] } :

ex a being set st
for b being set holds
( P₁[a] & P₂[b] )

provided

A1: for b being set ex a being set st
( P₁[a] & P₂[b] )

proof end;

scheme :: SCHEMS_1:sch 12
Schemat28{ P₁[ set , set ] } :

ex b being set st
for a being set holds P₁[a,b]

provided

A1: for a, b being set holds P₁[a,b]

proof end;

scheme :: SCHEMS_1:sch 13
Schemat30{ P₁[ set , set ] } :

ex a being set st P₁[a,a]

provided

A1: ex a being set st
for b being set holds P₁[a,b]

proof end;

scheme :: SCHEMS_1:sch 14
Schemat31{ P₁[ set , set ] } :

for a being set ex b being set st P₁[b,a]

provided

A1: for a being set holds P₁[a,a]

proof end;

scheme :: SCHEMS_1:sch 15
Schemat33{ P₁[ set , set ] } :

for a being set ex b being set st P₁[a,b]

provided

A1: for a being set holds P₁[a,a]

proof end;

scheme :: SCHEMS_1:sch 16
Schemat36{ P₁[ set , set ] } :

ex a, b being set st P₁[a,b]

provided

A1: for b being set ex a being set st P₁[a,b]

proof end;