mmtheorems19 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 1801-1900 - Page 19 of 123

Type	Label	Description
Statement
Theorem	r19.28av 1801	Restricted version of one direction of Theorem 19.28 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.)
|- ((ph /\ A.x e. A ps) -> A.x e. A (ph /\ ps))
Theorem	r19.29 1802	Theorem 19.29 of [Margaris] p. 90 with restricted quantifiers.
|- ((A.x e. A ph /\ E.x e. A ps) -> E.x e. A (ph /\ ps))
Theorem	r19.29r 1803	Variation of Theorem 19.29 of [Margaris] p. 90 with restricted quantifiers.
|- ((E.x e. A ph /\ A.x e. A ps) -> E.x e. A (ph /\ ps))
Theorem	r19.32v 1804	Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers.
|- (A.x e. A (ph \/ ps) <-> (ph \/ A.x e. A ps))
Theorem	r19.35 1805	Restricted quantifier version of Theorem 19.35 of [Margaris] p. 90.
|- (E.x e. A (ph -> ps) <-> (A.x e. A ph -> E.x e. A ps))
Theorem	r19.36av 1806	One direction of a restricted quantifier version of Theorem 19.36 of [Margaris] p. 90. The other direction doesn't hold when A is empty.
|- (E.x e. A (ph -> ps) -> (A.x e. A ph -> ps))
Theorem	r19.37av 1807	Restricted version of one direction of Theorem 19.37 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.)
|- (E.x e. A (ph -> ps) -> (ph -> E.x e. A ps))
Theorem	r19.40 1808	Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90.
|- (E.x e. A (ph /\ ps) -> (E.x e. A ph /\ E.x e. A ps))
Theorem	r19.41v 1809	Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
|- (E.x e. A (ph /\ ps) <-> (E.x e. A ph /\ ps))
Theorem	r19.42v 1810	Restricted version of Theorem 19.42 of [Margaris] p. 90.
|- (E.x e. A (ph /\ ps) <-> (ph /\ E.x e. A ps))
Theorem	r19.43 1811	Restricted version of Theorem 19.43 of [Margaris] p. 90.
|- (E.x e. A (ph \/ ps) <-> (E.x e. A ph \/ E.x e. A ps))
Theorem	r19.44av 1812	One direction of a restricted quantifier version of Theorem 19.44 of [Margaris] p. 90. The other direction doesn't hold when A is empty.
|- (E.x e. A (ph \/ ps) -> (E.x e. A ph \/ ps))
Theorem	r19.45av 1813	Restricted version of one direction of Theorem 19.45 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.)
|- (E.x e. A (ph \/ ps) -> (ph \/ E.x e. A ps))
Theorem	hbreu1 1814	x is not free in E!x e. Aph.
|- (E!x e. A ph -> A.xE!x e. A ph)
Theorem	rabid 1815	An "identity" law of concretion for restricted abstraction. Special case of Definition 2.1 of [Quine] p. 16.
|- (x e. {x e. A | ph} <-> (x e. A /\ ph))
Theorem	rabid2 1816	An "identity" law for restricted class abstraction.
|- (A = {x e. A | ph} <-> A.x e. A ph)
Theorem	rabswap 1817	Swap with a membership relation in a restricted class abstraction.
|- {x e. A | x e. B} = {x e. B | x e. A}
Theorem	hbrab1 1818	The abstraction variable in a restricted class abstraction isn't free.
|- (y e. {x e. A | ph} -> A.x y e. {x e. A | ph})
Theorem	hbrab 1819	A variable not free in a wff remains so in a restricted class abstraction.
|- (ph -> A.xph)   &   |- (z e. A -> A.x z e. A)   =>   |- (z e. {y e. A | ph} -> A.x z e. {y e. A | ph})
Theorem	ralcom 1820	Commutation of restricted quantifiers.
|- (A.x e. A A.y e. B ph <-> A.y e. B A.x e. A ph)
Theorem	rexcom 1821	Commutation of restricted quantifiers.
|- (E.x e. A E.y e. B ph <-> E.y e. B E.x e. A ph)
Theorem	ralcom2 1822	Commutation of restricted quantifiers. Note that x and y needn't be distinct (this makes the proof longer but illustrates the use of dvelim 1391).
|- (A.x e. A A.y e. A ph -> A.y e. A A.x e. A ph)
Theorem	ralcom3 1823	A commutative law for restricted quantifiers that swaps the domain of the restriction.
|- (A.x e. A (x e. B -> ph) <-> A.x e. B (x e. A -> ph))
Theorem	reeanv 1824	Rearrange existential quantifiers.
|- (E.x e. A E.y e. B (ph /\ ps) <-> (E.x e. A ph /\ E.y e. B ps))
Theorem	reubidva 1825	Formula-building rule for restricted existential quantifier (deduction rule).
|- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (E!x e. A ps <-> E!x e. A ch))
Theorem	reubidv 1826	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E!x e. A ps <-> E!x e. A ch))
Theorem	reubiia 1827	Formula-building rule for restricted existential quantifier (inference rule).
|- (x e. A -> (ph <-> ps))   =>   |- (E!x e. A ph <-> E!x e. A ps)
Theorem	reubii 1828	Formula-building rule for restricted existential quantifier (inference rule).
|- (ph <-> ps)   =>   |- (E!x e. A ph <-> E!x e. A ps)
Theorem	raleq1f 1829	Equality theorem for restricted universal quantifier, with bound-variable hypotheses instead of distinct variable restrictions.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (A = B -> (A.x e. A ph <-> A.x e. B ph))
Theorem	rexeq1f 1830	Equality theorem for restricted existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (A = B -> (E.x e. A ph <-> E.x e. B ph))
Theorem	reueq1f 1831	Equality theorem for restricted uniqueness quantifier, with bound-variable hypotheses instead of distinct variable restrictions.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (A = B -> (E!x e. A ph <-> E!x e. B ph))
Theorem	raleq1 1832	Equality theorem for restricted universal quantifier.
|- (A = B -> (A.x e. A ph <-> A.x e. B ph))
Theorem	rexeq1 1833	Equality theorem for restricted existential quantifier.
|- (A = B -> (E.x e. A ph <-> E.x e. B ph))
Theorem	reueq1 1834	Equality theorem for restricted uniqueness quantifier.
|- (A = B -> (E!x e. A ph <-> E!x e. B ph))
Theorem	raleq1d 1835	Equality deduction for restricted universal quantifier.
|- (ph -> A = B)   =>   |- (ph -> (A.x e. A ps <-> A.x e. B ps))
Theorem	rexeq1d 1836	Equality deduction for restricted existential quantifier.
|- (ph -> A = B)   =>   |- (ph -> (E.x e. A ps <-> E.x e. B ps))
Theorem	raleqd 1837	Equality deduction for restricted universal quantifier.
|- (A = B -> (ph <-> ps))   =>   |- (A = B -> (A.x e. A ph <-> A.x e. B ps))
Theorem	rexeqd 1838	Equality deduction for restricted existential quantifier.
|- (A = B -> (ph <-> ps))   =>   |- (A = B -> (E.x e. A ph <-> E.x e. B ps))
Theorem	reueqd 1839	Equality deduction for restricted uniqueness quantifier.
|- (A = B -> (ph <-> ps))   =>   |- (A = B -> (E!x e. A ph <-> E!x e. B ps))
Theorem	raleq12d 1840	Equality deduction for restricted universal quantifier.
|- (ph -> A = B)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. B ch))
Theorem	rexeq12d 1841	Equality deduction for restricted universal quantifier.
|- (ph -> A = B)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. B ch))
Theorem	cbvralf 1842	Rule used to change bound variables, using implicit substitition.
|- (z e. A -> A.x z e. A)   &   |- (z e. A -> A.y z e. A)   &   |- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (A.x e. A ph <-> A.y e. A ps)
Theorem	cbvrexf 1843	Rule used to change bound variables, using implicit substitition. (Contributed by FL, 27-Apr-2008.)
|- (z e. A -> A.x z e. A)   &   |- (z e. A -> A.y z e. A)   &   |- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (E.x e. A ph <-> E.y e. A ps)
Theorem	cbvral 1844	Rule used to change bound variables, using implicit substitition.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (A.x e. A ph <-> A.y e. A ps)
Theorem	cbvrex 1845	Rule used to change bound variables, using implicit substitition.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (E.x e. A ph <-> E.y e. A ps)
Theorem	cbvralv 1846	Change the bound variable of a restricted universal quantifier using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (A.x e. A ph <-> A.y e. A ps)
Theorem	cbvrexv 1847	Change the bound variable of a restricted existential quantifier using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (E.x e. A ph <-> E.y e. A ps)
Theorem	cbvreuv 1848	Change the bound variable of a restricted uniqueness quantifier using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (E!x e. A ph <-> E!y e. A ps)
Theorem	cbvral2v 1849	Change bound variables of double restricted universal quantification, using implicit substitution.
|- (x = z -> (ph <-> ch))   &   |- (y = w -> (ch <-> ps))   =>   |- (A.x e. A A.y e. B ph <-> A.z e. A A.w e. B ps)
Theorem	cbvral3v 1850	Change bound variables of triple restricted universal quantification, using implicit substitution.
|- (x = w -> (ph <-> ch))   &   |- (y = v -> (ch <-> th))   &   |- (z = u -> (th <-> ps))   =>   |- (A.x e. A A.y e. B A.z e. C ph <-> A.w e. A A.v e. B A.u e. C ps)
Theorem	rabbii 1851	Equivalent wff's yield equal restricted class abstractions (inference rule).
|- (x e. A -> (ps <-> ch))   =>   |- {x e. A | ps} = {x e. A | ch}
Theorem	rabbidv 1852	Equivalent wff's yield equal restricted class abstractions (deduction rule).
|- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> {x e. A | ps} = {x e. A | ch})
Theorem	rabbisdv 1853	Equivalent wff's yield equal restricted class abstractions (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> {x e. A | ps} = {x e. A | ch})
Theorem	rabeqf 1854	Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (A = B -> {x e. A | ph} = {x e. B | ph})
Theorem	rabeq 1855	Equality theorem for restricted class abstractions.
|- (A = B -> {x e. A | ph} = {x e. B | ph})
Theorem	rabeq2i 1856	Inference rule from equality of a class variable and a restricted class abstraction.
|- A = {x e. B | ph}   =>   |- (x e. A <-> (x e. B /\ ph))
The universal class
Syntax	cvv 1857	Extend class notation to include the universal class symbol.
class V
Definition	df-v 1858	Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21.
|- V = {x | x = x}
Theorem	visset 1859	All set variables are sets (see isset 1860). Theorem 6.8 of [Quine] p. 43.
|- x e. V
Theorem	isset 1860	Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 1858) if and only if the class A exists (i.e. there exists some set x equal to class A). Theorem 6.9 of [Quine] p. 43. Notational convention: We will use the notational device "A e. V" to mean "A is a set" very frequently, for example in uniex 3093. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 3094, in order to shorten certain proofs we use the more general antecedent A e. B instead of A e. V to mean "A is a set." Note that a constant is considered distinct from all variables. This is why V is not included in the distinct variable list, even though df-clel 1514 requires that the expression substituted for B not contain x. (Also, the Metamath spec does not allow constants in the distinct variable list.)
|- (A e. V <-> E.x x = A)
Theorem	isseti 1861	A way to say "A is a set" (inference rule).
|- A e. V   =>   |- E.x x = A
Theorem	issetri 1862	A way to say "A is a set" (inference rule).
|- E.x x = A   =>   |- A e. V
Theorem	elisset 1863	If a class is a member of another class, it is a set. Theorem 6.12 of [Quine] p. 44.
|- (A e. B -> A e. V)
Theorem	elisseti 1864	If a class is a member of another class, it is a set.
|- A e. B   =>   |- A e. V
Theorem	elex 1865	An element of a class exists.
|- (A e. B -> E.x x = A)
Theorem	ralv 1866	A universal quantifier restricted to the universe is unrestricted.
|- (A.x e. V ph <-> A.xph)
Theorem	rexv 1867	An existential quantifier restricted to the universe is unrestricted.
|- (E.x e. V ph <-> E.xph)
Theorem	rabab 1868	A class abstraction restricted to the universe is unrestricted.
|- {x e. V | ph} = {x | ph}
Theorem	ralcom4 1869	Commutation of restricted and unrestricted universal quantifiers.
|- (A.x e. A A.yph <-> A.yA.x e. A ph)
Theorem	rexcom4 1870	Commutation of restricted and unrestricted existential quantifiers.
|- (E.x e. A E.yph <-> E.yE.x e. A ph)
Theorem	ceqsalg 1871	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis.
|- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A.x(x = A -> ph) <-> ps))
Theorem	ceqsal 1872	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis.
|- (ps -> A.xps)   &   |- A e. V   &   |- (x = A -> (ph <-> ps))   =>   |- (A.x(x = A -> ph) <-> ps)
Theorem	ceqsalv 1873	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis.
|- A e. V   &   |- (x = A -> (ph <-> ps))   =>   |- (A.x(x = A -> ph) <-> ps)
Theorem	gencl 1874	Implicit substitution for class with embedded variable.
|- (th <-> E.x(ch /\ A = B))   &   |- (A = B -> (ph <-> ps))   &   |- (ch -> ph)   =>   |- (th -> ps)
Theorem	2gencl 1875	Implicit substitution for class with embedded variable.
|- (C e. S <-> E.x(x e. R /\ A = C))   &   |- (D e. S <-> E.y(y e. R /\ B = D))   &   |- (A = C -> (ph <-> ps))   &   |- (B = D -> (ps <-> ch))   &   |- ((x e. R /\ y e. R) -> ph)   =>   |- ((C e. S /\ D e. S) -> ch)
Theorem	3gencl 1876	Implicit substitution for class with embedded variable.
|- (D e. S <-> E.x(x e. R /\ A = D))   &   |- (F e. S <-> E.y(y e. R /\ B = F))   &   |- (G e. S <-> E.z(z e. R /\ C = G))   &   |- (A = D -> (ph <-> ps))   &   |- (B = F -> (ps <-> ch))   &   |- (C = G -> (ch <-> th))   &   |- ((x e. R /\ y e. R /\ z e. R) -> ph)   =>   |- ((D e. S /\ F e. S /\ G e. S) -> th)
Theorem	cgsexg 1877	Implicit substitution inference for general classes.
|- (x = A -> ch)   &   |- (ch -> (ph <-> ps))   =>   |- (A e. B -> (E.x(ch /\ ph) <-> ps))
Theorem	cgsex2g 1878	Implicit substitution inference for general classes.
|- ((x = A /\ y = B) -> ch)   &   |- (ch -> (ph <-> ps))   =>   |- ((A e. C /\ B e. D) -> (E.xE.y(ch /\ ph) <-> ps))
Theorem	cgsex4g 1879	An implicit substitution inference for 4 general classes.
|- (((x = A /\ y = B) /\ (z = C /\ w = D)) -> ch)   &   |- (ch -> (ph <-> ps))   =>   |- (((A e. R /\ B e. S) /\ (C e. R /\ D e. S)) -> (E.xE.yE.zE.w(ch /\ ph) <-> ps))
Theorem	ceqsex 1880	Elimination of an existential quantifier, using implicit substitution.
|- (ps -> A.xps)   &   |- A e. V   &   |- (x = A -> (ph <-> ps))   =>   |- (E.x(x = A /\ ph) <-> ps)
Theorem	ceqsexv 1881	Elimination of an existential quantifier, using implicit substitution.
|- A e. V   &   |- (x = A -> (ph <-> ps))   =>   |- (E.x(x = A /\ ph) <-> ps)
Theorem	ceqsex2 1882	Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.)
|- (ps -> A.xps)   &   |- (ch -> A.ych)   &   |- A e. V   &   |- B e. V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- (E.xE.y((x = A /\ y = B) /\ ph) <-> ch)
Theorem	ceqsex2v 1883	Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.)
|- A e. V   &   |- B e. V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- (E.xE.y((x = A /\ y = B) /\ ph) <-> ch)
Theorem	gencbvex 1884	Change of bound variable using implicit substitution.
|- A e. V   &   |- (A = y -> (ph <-> ps))   &   |- (A = y -> (ch <-> th))   &   |- (th <-> E.x(ch /\ A = y))   =>   |- (E.x(ch /\ ph) <-> E.y(th /\ ps))
Theorem	gencbvex2 1885	Restatement of gencbvex 1884 with weaker hypotheses. (Contributed by Jeffrey Hankins, 6-Dec-2006.)
|- A e. V   &   |- (A = y -> (ph <-> ps))   &   |- (A = y -> (ch <-> th))   &   |- (th -> E.x(ch /\ A = y))   =>   |- (E.x(ch /\ ph) <-> E.y(th /\ ps))
Theorem	gencbval 1886	Change of bound variable using implicit substitution.
|- A e. V   &   |- (A = y -> (ph <-> ps))   &   |- (A = y -> (ch <-> th))   &   |- (th <-> E.x(ch /\ A = y))   =>   |- (A.x(ch -> ph) <-> A.y(th -> ps))
Theorem	vtoclf 1887	Implicit substitution of a class for a set variable. This is a generalization of chvar 1204.
|- (ps -> A.xps)   &   |- A e. V   &   |- (x = A -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl 1888	Implicit substitution of a class for a set variable.
|- A e. V   &   |- (x = A -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl2 1889	Implicit substitution of classes for set variables.
|- A e. V   &   |- B e. V   &   |- ((x = A /\ y = B) -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl3 1890	Implicit substitution of classes for set variables.
|- A e. V   &   |- B e. V   &   |- C e. V   &   |- ((x = A /\ y = B /\ z = C) -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtoclb 1891	Implicit substitution of a class for a set variable.
|- A e. V   &   |- (x = A -> (ph <-> ch))   &   |- (x = A -> (ps <-> th))   &   |- (ph <-> ps)   =>   |- (ch <-> th)
Theorem	vtoclgf 1892	Implicit substitution of a class for a set variable, with bound-variable hypotheses in place of distinct variable restrictions.
|- (y e. A -> A.x y e. A)   &   |- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   &   |- ph   =>   |- (A e. B -> ps)
Theorem	vtoclg 1893	Implicit substitution of a class for a set variable.
|- (x = A -> (ph <-> ps))   &   |- ph   =>   |- (A e. B -> ps)
Theorem	vtoclbg 1894	Implicit substitution of a class for a set variable.
|- (x = A -> (ph <-> ch))   &   |- (x = A -> (ps <-> th))   &   |- (ph <-> ps)   =>   |- (A e. B -> (ch <-> th))
Theorem	vtocl2gf 1895	Implicit substitution of a class for a set variable.
|- (ps -> A.xps)   &   |- (ch -> A.ych)   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- ph   =>   |- ((A e. C /\ B e. D) -> ch)
Theorem	vtocl2g 1896	Implicit substitution of 2 classes for 2 set variables.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- ph   =>   |- ((A e. C /\ B e. D) -> ch)
Theorem	vtoclgaf 1897	Implicit substitution of a class for a set variable.
|- (y e. A -> A.x y e. A)   &   |- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   &   |- (x e. B -> ph)   =>   |- (A e. B -> ps)
Theorem	vtoclga 1898	Implicit substitution of a class for a set variable.
|- (x = A -> (ph <-> ps))   &   |- (x e. B -> ph)   =>   |- (A e. B -> ps)
Theorem	vtocl2ga 1899	Implicit substitution of 2 classes for 2 set variables.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- ((x e. C /\ y e. D) -> ph)   =>   |- ((A e. C /\ B e. D) -> ch)
Theorem	vtocl3ga 1900	Implicit substitution of 3 classes for 3 set variables.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   &   |- ((x e. D /\ y e. R /\ z e. S) -> ph)   =>   |- ((A e. D /\ B e. R /\ C e. S) -> th)