:: Schemes
:: by Stanis\l aw T. Czuba
::
:: Copyright (c) 1990-2021 Association of Mizar Users

scheme :: SCHEMS_1:sch 1
Schemat0{ P1[ set ] } :
ex a being set st P1[a]
provided
A1: for a being set holds P1[a]
proof end;

scheme :: SCHEMS_1:sch 2
Schemat3{ P1[ set , set ] } :
for b being set ex a being set st P1[a,b]
provided
A1: ex a being set st
for b being set holds P1[a,b]
proof end;

scheme :: SCHEMS_1:sch 3
Schemat8{ P1[ set ], P2[ set ] } :
( ( for a being set holds P1[a] ) implies for a being set holds P2[a] )
provided
A1: for a being set st P1[a] holds
P2[a]
proof end;

scheme :: SCHEMS_1:sch 4
Schemat9{ P1[ set ], P2[ set ] } :
( ( for a being set holds P1[a] ) iff for a being set holds P2[a] )
provided
A1: for a being set holds
( P1[a] iff P2[a] )
proof end;

scheme :: SCHEMS_1:sch 5
Schemat17{ P1[ set ], P2[] } :
( ( for a being set holds P1[a] ) implies P2[] )
provided
A1: for a being set st P1[a] holds
P2[]
proof end;

scheme :: SCHEMS_1:sch 6
Schemat18a{ P1[ set ], P2[ set ] } :
ex a being set st
for b being set holds
( P1[a] or P2[b] )
provided
A1: ( ex a being set st P1[a] or for b being set holds P2[b] )
proof end;

scheme :: SCHEMS_1:sch 7
Schemat18b{ P1[ set ], P2[ set ] } :
( ex a being set st P1[a] or for b being set holds P2[b] )
provided
A1: ex a being set st
for b being set holds
( P1[a] or P2[b] )
proof end;

scheme :: SCHEMS_1:sch 8
Schemat20b{ P1[ set ], P2[ set ] } :
ex a being set st
for b being set holds
( P1[a] or P2[b] )
provided
A1: for b being set ex a being set st
( P1[a] or P2[b] )
proof end;

scheme :: SCHEMS_1:sch 9
Schemat22a{ P1[ set ], P2[ set ] } :
for b being set ex a being set st
( P1[a] & P2[b] )
provided
A1: ( ex a being set st P1[a] & ( for b being set holds P2[b] ) )
proof end;

scheme :: SCHEMS_1:sch 10
Schemat22b{ P1[ set ], P2[ set ] } :
( ex a being set st P1[a] & ( for b being set holds P2[b] ) )
provided
A1: for b being set ex a being set st
( P1[a] & P2[b] )
proof end;

scheme :: SCHEMS_1:sch 11
Schemat23b{ P1[ set ], P2[ set ] } :
ex a being set st
for b being set holds
( P1[a] & P2[b] )
provided
A1: for b being set ex a being set st
( P1[a] & P2[b] )
proof end;

scheme :: SCHEMS_1:sch 12
Schemat28{ P1[ set , set ] } :
ex b being set st
for a being set holds P1[a,b]
provided
A1: for a, b being set holds P1[a,b]
proof end;

scheme :: SCHEMS_1:sch 13
Schemat30{ P1[ set , set ] } :
ex a being set st P1[a,a]
provided
A1: ex a being set st
for b being set holds P1[a,b]
proof end;

scheme :: SCHEMS_1:sch 14
Schemat31{ P1[ set , set ] } :
for a being set ex b being set st P1[b,a]
provided
A1: for a being set holds P1[a,a]
proof end;

scheme :: SCHEMS_1:sch 15
Schemat33{ P1[ set , set ] } :
for a being set ex b being set st P1[a,b]
provided
A1: for a being set holds P1[a,a]
proof end;

scheme :: SCHEMS_1:sch 16
Schemat36{ P1[ set , set ] } :
ex a, b being set st P1[a,b]
provided
A1: for b being set ex a being set st P1[a,b]
proof end;