The abstract of the Mizar article:

Schemes

by

Stanislaw T. Czuba

Received December 17, 1990

MML identifier: SCHEMS_1

[ Mizar article, MML identifier index ]

environ

 constructors XBOOLE_0;
 clusters XBOOLE_0;


begin

reserve a,b,d for set;

scheme Schemat0 {P[set]} :
   ex a st P[a]
    provided
 for a holds P[a];

scheme Schemat1a {P[set],T[]} :
   (for a holds P[a]) & T[]
    provided
 for a holds (P[a] & T[]);

scheme Schemat1b {P[set],T[]} :
   for a holds (P[a] & T[])
    provided
 (for a holds P[a]) & T[];

scheme Schemat2a {P[set], T[]} :
   (ex a st P[a]) or T[]
    provided
 ex a st (P[a] or T[]);

scheme Schemat2b {P[set], T[]} :
   ex a st (P[a] or T[])
    provided
 (ex a st P[a]) or T[];

scheme Schemat3 {S[set,set]} :
   for b ex a st S[a,b]
    provided
 ex a st for b holds S[a,b];

scheme Schemat4a {P[set],Q[set]} :
   (ex a st P[a]) or (ex a st Q[a])
    provided
 ex a st (P[a] or Q[a]);

scheme Schemat4b {P[set],Q[set]} :
   ex a st (P[a] or Q[a])
    provided
 (ex a st P[a]) or (ex a st Q[a]);

scheme Schemat5 {P[set],Q[set]} :
(ex a st P[a]) & (ex a st Q[a])
    provided
 ex a st (P[a] & Q[a]);

scheme Schemat6a {P[set],Q[set]} :
   (for a holds P[a]) & (for a holds Q[a])
    provided
 for a holds (P[a] & Q[a]);

scheme Schemat6b {P[set],Q[set]} :
   for a holds (P[a] & Q[a])
    provided
 (for a holds P[a]) & (for a holds Q[a]);

scheme Schemat7 {P[set],Q[set]} :
   for a holds (P[a] or Q[a])
    provided
 (for a holds P[a]) or (for a holds Q[a]);

scheme Schemat8 {P[set],Q[set]} :
   (for a holds P[a]) implies (for a holds Q[a])
    provided
 for a holds P[a] implies Q[a];

scheme Schemat9 {P[set],Q[set]} :
   (for a holds P[a]) iff (for a holds Q[a])
    provided
 for a holds (P[a] iff Q[a]);

scheme Schemat10b {T[]} :
   for a holds T[]
    provided
 T[];

scheme Schemat11a {P[set],T[]} :
   (for a holds P[a]) or T[]
    provided
 for a holds (P[a] or T[]);

scheme Schemat11b {P[set],T[]} :
   for a holds (P[a] or T[])
    provided
 (for a holds P[a]) or T[];

scheme Schemat12a {P[set],T[]} :
   ex a st (T[] & P[a])
    provided
 T[] & (ex a st P[a]);

scheme Schemat12b {P[set],T[]} :
   T[] & (ex a st P[a])
    provided
 ex a st (T[] & P[a]);

scheme Schemat13a {P[set],T[]} :
   for a holds (T[] implies P[a])
    provided
 T[] implies (for a holds P[a]);

scheme Schemat13b {P[set],T[]} :
   T[] implies (for a holds P[a])
    provided
 for a holds (T[] implies P[a]);

scheme Schemat14 {P[set],T[]} :
   ex a st (T[] implies P[a])
    provided
 T[] implies (ex a st P[a]);

scheme Schemat17 {P[set],T[]} :
   (for a holds P[a]) implies T[]
    provided
 for a holds (P[a] implies T[]);

scheme Schemat18a {P[set],Q[set]} :
   ex a st (for b holds (P[a] or Q[b]))
    provided
 (ex a st P[a]) or (for b holds Q[b]);

scheme Schemat18b {P[set],Q[set]} :
   (ex a st P[a]) or (for b holds Q[b])
    provided
 ex a st for b holds (P[a] or Q[b]);

scheme Schemat19a {P[set],Q[set]} :
   for b holds (ex a st (P[a] or Q[b]))
    provided
 (ex a st P[a]) or (for b holds Q[b]);

scheme Schemat19b {P[set],Q[set]} :
   (ex a st P[a]) or (for b holds Q[b])
    provided
 for b holds (ex a st (P[a] or Q[b]));

scheme Schemat20b {P[set],Q[set]} :
   ex a st (for b holds (P[a] or Q[b]))
    provided
 for b ex a st (P[a] or Q[b]);

scheme Schemat21a {P[set],Q[set]} :
   ex a st for b holds P[a] & Q[b]
    provided
 (ex a st P[a]) & (for b holds Q[b]);

scheme Schemat21b {P[set],Q[set]} :
   (ex a st P[a]) & (for b holds Q[b])
    provided
 ex a st for b holds P[a] & Q[b];

scheme Schemat22a {P[set],Q[set]} :
   for b ex a st (P[a] & Q[b])
    provided
 (ex a st P[a]) & (for b holds Q[b]);

scheme Schemat22b {P[set],Q[set]} :
   (ex a st P[a]) & (for b holds Q[b])
    provided
 for b ex a st P[a] & Q[b];

scheme Schemat23b {P[set],Q[set]} :
   ex a st for b holds P[a] & Q[b]
    provided
 for b ex a st P[a] & Q[b];

scheme Schemat24a {S[set,set],Q[set]} :
   for a ex b st (S[a,b] implies Q[a])
    provided
 for a holds ((for b holds S[a,b]) implies Q[a]);

scheme Schemat24b {S[set,set],Q[set]} :
   for a holds ((for b holds S[a,b]) implies Q[a])
    provided
 for a ex b st (S[a,b] implies Q[a]);

scheme Schemat25a {S[set,set],Q[set]} :
   for a,b holds (S[a,b] implies Q[a])
    provided
 for a holds ((ex b st S[a,b]) implies Q[a]);

scheme Schemat25b {S[set,set],Q[set]} :
   for a holds ((ex b st S[a,b]) implies Q[a])
    provided
 for a,b holds (S[a,b] implies Q[a]);

scheme Schemat27 {S[set,set]} :
   for a holds S[a,a]
    provided
 for a,b holds S[a,b];

scheme Schemat28 {S[set,set]} :
   ex b st for a holds S[a,b]
    provided
 for a,b holds S[a,b];

scheme Schemat30 {S[set,set]} :
   ex a st S[a,a]
    provided
 ex a st for b holds S[a,b];

scheme Schemat31 {S[set,set]} :
   for a ex b st S[b,a]
    provided
 for a holds S[a,a];

scheme Schemat33 {S[set,set]} :
   for a ex b st S[a,b]
    provided
 for a holds S[a,a];

scheme Schemat36 {S[set,set]} :
   ex a,b st S[a,b]
    provided
 for b ex a st S[a,b];

scheme Schemat37 {S[set,set]} :
   ex a,b st S[a,b]
    provided
 ex a st S[a,a];