mmtheorems24 - 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-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 2301-2400 - Page 24 of 175

Type	Label	Description
Statement
Theorem	elisseti 2301	If a class is a member of another class, it is a set.
|- A e. B   =>   |- A e. _V
Theorem	elex 2302	An element of a class exists.
|- (A e. B -> E.x x = A)
Theorem	elex22 2303	If two classes each contain another class, then both contain some set. This proof was automatically generated from the virtual deduction proof elex22VD 16663 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.)
|- ((A e. B /\ A e. C) -> E.x(x e. B /\ x e. C))
Theorem	elex2 2304	If a class contains another class, then it contains some set. This proof was generated automatically from the virtual deduction proof elex2 2304 using the tools command file translatewithout_overwritingminimize_excludingduplicates.cmd . (Contributed by Alan Sare, 25-Sep-2011.)
|- (A e. B -> E.x x e. B)
Theorem	ralv 2305	A universal quantifier restricted to the universe is unrestricted.
|- (A.x e. _V ph <-> A.xph)
Theorem	rexv 2306	An existential quantifier restricted to the universe is unrestricted.
|- (E.x e. _V ph <-> E.xph)
Theorem	reuv 2307	A uniqueness quantifier restricted to the universe is unrestricted.
|- (E!x e. _V ph <-> E!xph)
Theorem	rabab 2308	A class abstraction restricted to the universe is unrestricted. (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- {x e. _V | ph} = {x | ph}
Theorem	rababOLD 2309	A class abstraction restricted to the universe is unrestricted.
|- {x e. _V | ph} = {x | ph}
Theorem	ralcom4 2310	Commutation of restricted and unrestricted universal quantifiers. (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- (A.x e. A A.yph <-> A.yA.x e. A ph)
Theorem	ralcom4OLD 2311	Commutation of restricted and unrestricted universal quantifiers.
|- (A.x e. A A.yph <-> A.yA.x e. A ph)
Theorem	rexcom4 2312	Commutation of restricted and unrestricted existential quantifiers. (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- (E.x e. A E.yph <-> E.yE.x e. A ph)
Theorem	rexcom4OLD 2313	Commutation of restricted and unrestricted existential quantifiers.
|- (E.x e. A E.yph <-> E.yE.x e. A ph)
Theorem	ceqsalg 2314	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A.x(x = A -> ph) <-> ps))
Theorem	ceqsalgOLD 2315	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 2316	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 2317	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 2318	Implicit substitution for class with embedded variable.
|- (th <-> E.x(ch /\ A = B))   &   |- (A = B -> (ph <-> ps))   &   |- (ch -> ph)   =>   |- (th -> ps)
Theorem	2gencl 2319	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 2320	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 2321	Implicit substitution inference for general classes.
|- (x = A -> ch)   &   |- (ch -> (ph <-> ps))   =>   |- (A e. B -> (E.x(ch /\ ph) <-> ps))
Theorem	cgsex2g 2322	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 2323	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 2324	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 2325	Elimination of an existential quantifier, using implicit substitution.
|- A e. _V   &   |- (x = A -> (ph <-> ps))   =>   |- (E.x(x = A /\ ph) <-> ps)
Theorem	ceqsex2 2326	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	ceqsex2OLD 2327	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 2328	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	ceqsex2vOLD 2329	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	ceqsex3v 2330	Elimination of three existential quantifiers, using implicit substitution.
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   =>   |- (E.xE.yE.z((x = A /\ y = B /\ z = C) /\ ph) <-> th)
Theorem	ceqsex4v 2331	Elimination of four existential quantifiers, using implicit substitution.
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- D e. _V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   &   |- (w = D -> (th <-> ta))   =>   |- (E.xE.yE.zE.w((x = A /\ y = B) /\ (z = C /\ w = D) /\ ph) <-> ta)
Theorem	ceqsex6v 2332	Elimination of six existential quantifiers, using implicit substitution.
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- D e. _V   &   |- E e. _V   &   |- F e. _V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   &   |- (w = D -> (th <-> ta))   &   |- (v = E -> (ta <-> et))   &   |- (u = F -> (et <-> ze))   =>   |- (E.xE.yE.zE.wE.vE.u((x = A /\ y = B /\ z = C) /\ (w = D /\ v = E /\ u = F) /\ ph) <-> ze)
Theorem	ceqsex8v 2333	Elimination of eight existential quantifiers, using implicit substitution.
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- D e. _V   &   |- E e. _V   &   |- F e. _V   &   |- G e. _V   &   |- H e. _V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   &   |- (w = D -> (th <-> ta))   &   |- (v = E -> (ta <-> et))   &   |- (u = F -> (et <-> ze))   &   |- (t = G -> (ze <-> si))   &   |- (s = H -> (si <-> rh))   =>   |- (E.xE.yE.zE.wE.vE.uE.tE.s(((x = A /\ y = B) /\ (z = C /\ w = D)) /\ ((v = E /\ u = F) /\ (t = G /\ s = H)) /\ ph) <-> rh)
Theorem	gencbvex 2334	Change of bound variable using implicit substitution. (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- 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	gencbvexOLD 2335	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 2336	Restatement of gencbvex 2334 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 2337	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 2338	Implicit substitution of a class for a set variable. This is a generalization of chvar 1530.
|- (ps -> A.xps)   &   |- A e. _V   &   |- (x = A -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl 2339	Implicit substitution of a class for a set variable.
|- A e. _V   &   |- (x = A -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl2 2340	Implicit substitution of classes for set variables. (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- A e. _V   &   |- B e. _V   &   |- ((x = A /\ y = B) -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl2OLD 2341	Implicit substitution of classes for set variables.
|- A e. _V   &   |- B e. _V   &   |- ((x = A /\ y = B) -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl3 2342	Implicit substitution of classes for set variables. (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- ((x = A /\ y = B /\ z = C) -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl3OLD 2343	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 2344	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 2345	Implicit substitution of a class for a set variable, with bound-variable hypotheses in place of distinct variable restrictions. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
|- (y e. A -> A.x y e. A)   &   |- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   &   |- ph   =>   |- (A e. B -> ps)
Theorem	vtoclg 2346	Implicit substitution of a class for a set variable.
|- (x = A -> (ph <-> ps))   &   |- ph   =>   |- (A e. B -> ps)
Theorem	vtoclbg 2347	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 2348	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 2349	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 2350	Implicit substitution of a class for a set variable. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 8-Jun-2011.)
|- (y e. A -> A.x y e. A)   &   |- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   &   |- (x e. B -> ph)   =>   |- (A e. B -> ps)
Theorem	vtoclgafOLD 2351	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 2352	Implicit substitution of a class for a set variable.
|- (x = A -> (ph <-> ps))   &   |- (x e. B -> ph)   =>   |- (A e. B -> ps)
Theorem	vtocl2ga 2353	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 2354	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)
Theorem	vtocleg 2355	Implicit substitution of a class for a set variable.
|- (x = A -> ph)   =>   |- (A e. B -> ph)
Theorem	vtoclegft 2356	Implicit substitution of a class for a set variable. (Closed theorem version of vtoclef 2358.) (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- ((A e. B /\ A.x(ph -> A.xph) /\ A.x(x = A -> ph)) -> ph)
Theorem	vtoclegftOLD 2357	Implicit substitution of a class for a set variable. (Closed theorem version of vtoclef 2358.)
|- ((A e. B /\ A.x(ph -> A.xph) /\ A.x(x = A -> ph)) -> ph)
Theorem	vtoclef 2358	Implicit substitution of a class for a set variable.
|- (ph -> A.xph)   &   |- A e. _V   &   |- (x = A -> ph)   =>   |- ph
Theorem	vtocle 2359	Implicit substitution of a class for a set variable.
|- A e. _V   &   |- (x = A -> ph)   =>   |- ph
Theorem	vtoclri 2360	Implicit substitution of a class for a set variable.
|- (x = A -> (ph <-> ps))   &   |- A.x e. B ph   =>   |- (A e. B -> ps)
Theorem	cla4gf 2361	Rule of specialization, using implicit substitition. Compare Theorem 7.3 of [Quine] p. 44. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 12-Aug-2011.)
|- (y e. A -> A.x y e. A)   &   |- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A.xph -> ps))
Theorem	cla4egf 2362	Existential specialization, using implicit substitition.
|- (y e. A -> A.x y e. A)   &   |- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (ps -> E.xph))
Theorem	cla4gfOLD 2363	Rule of specialization, using implicit substitition. Compare Theorem 7.3 of [Quine] p. 44.
|- (y e. A -> A.x y e. A)   &   |- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A.xph -> ps))
Theorem	cla4gv 2364	Rule of specialization, using implicit substitition. Compare Theorem 7.3 of [Quine] p. 44.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A.xph -> ps))
Theorem	cla4egv 2365	Existential specialization, using implicit substitition.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (ps -> E.xph))
Theorem	cla42egv 2366	Existential specialization with 2 quantifiers, using implicit substitution.
|- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- ((A e. C /\ B e. D) -> (ps -> E.xE.yph))
Theorem	cla42gv 2367	Specialization with 2 quantifiers, using implicit substitution.
|- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- ((A e. C /\ B e. D) -> (A.xA.yph -> ps))
Theorem	cla43egv 2368	Existential specialization with 3 quantifiers, using implicit substitution.
|- ((x = A /\ y = B /\ z = C) -> (ph <-> ps))   =>   |- ((A e. R /\ B e. S /\ C e. T) -> (ps -> E.xE.yE.zph))
Theorem	cla43gv 2369	Specialization with 3 quantifiers, using implicit substitution.
|- ((x = A /\ y = B /\ z = C) -> (ph <-> ps))   =>   |- ((A e. R /\ B e. S /\ C e. T) -> (A.xA.yA.zph -> ps))
Theorem	cla4v 2370	Rule of specialization, using implicit substitition.
|- A e. _V   &   |- (x = A -> (ph <-> ps))   =>   |- (A.xph -> ps)
Theorem	cla4ev 2371	Existential specialization, using implicit substitition. (The proof was shortened by Eric Schmidt, 22-Dec-2006.)
|- A e. _V   &   |- (x = A -> (ph <-> ps))   =>   |- (ps -> E.xph)
Theorem	cla42ev 2372	Existential specialization, using implicit substitition.
|- A e. _V   &   |- B e. _V   &   |- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- (ps -> E.xE.yph)
Theorem	rcla4 2373	Restricted specialization, using implicit substitition. (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A.x e. B ph -> ps))
Theorem	rcla4OLD 2374	Restricted specialization, using implicit substitition.
|- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A.x e. B ph -> ps))
Theorem	rcla4e 2375	Restricted existential specialization, using implicit substitition.
|- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- ((A e. B /\ ps) -> E.x e. B ph)
Theorem	rcla4v 2376	Restricted specialization, using implicit substitition.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A.x e. B ph -> ps))
Theorem	rcla4cv 2377	Restricted specialization, using implicit substitition.
|- (x = A -> (ph <-> ps))   =>   |- (A.x e. B ph -> (A e. B -> ps))
Theorem	rcla4va 2378	Restricted specialization, using implicit substitition.
|- (x = A -> (ph <-> ps))   =>   |- ((A e. B /\ A.x e. B ph) -> ps)
Theorem	rcla4cva 2379	Restricted specialization, using implicit substitition. (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- (x = A -> (ph <-> ps))   =>   |- ((A.x e. B ph /\ A e. B) -> ps)
Theorem	rcla4cvaOLD 2380	Restricted specialization, using implicit substitition.
|- (x = A -> (ph <-> ps))   =>   |- ((A.x e. B ph /\ A e. B) -> ps)
Theorem	rcla4ev 2381	Restricted existential specialization, using implicit substitition.
|- (x = A -> (ph <-> ps))   =>   |- ((A e. B /\ ps) -> E.x e. B ph)
Theorem	rcla4dv 2382	Restricted specialization, using implicit substitition.
|- ((ph /\ x = A) -> (ps <-> ch))   =>   |- ((ph /\ A e. B) -> (A.x e. B ps -> ch))
Theorem	rcla4edv 2383	Restricted existential specialization, using implicit substitition. (Contributed by FL, 17-Apr-2007.)
|- ((ph /\ x = A) -> (ps <-> ch))   =>   |- ((ph /\ A e. B) -> (ch -> E.x e. B ps))
Theorem	rcla42v 2384	2-variable restricted specialization, using implicit substitition.
|- (x = A -> (ph <-> ch))   &   |- (y = B -> (ch <-> ps))   =>   |- ((A e. C /\ B e. D) -> (A.x e. C A.y e. D ph -> ps))
Theorem	rcla42ev 2385	2-variable restricted existential specialization, using implicit substitution.
|- (x = A -> (ph <-> ch))   &   |- (y = B -> (ch <-> ps))   =>   |- ((A e. C /\ B e. D /\ ps) -> E.x e. C E.y e. D ph)
Theorem	rcla43v 2386	3-variable restricted specialization, using implicit substitition.
|- (x = A -> (ph <-> ch))   &   |- (y = B -> (ch <-> th))   &   |- (z = C -> (th <-> ps))   =>   |- ((A e. R /\ B e. S /\ C e. T) -> (A.x e. R A.y e. S A.z e. T ph -> ps))
Theorem	eqvinc 2387	A variable introduction law for class equality. (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- A e. _V   =>   |- (A = B <-> E.x(x = A /\ x = B))
Theorem	eqvincOLD 2388	A variable introduction law for class equality.
|- A e. _V   =>   |- (A = B <-> E.x(x = A /\ x = B))
Theorem	eqvincf 2389	A variable introduction law for class equality, using bound-variable hypotheses instead of distinct variable conditions.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   &   |- A e. _V   =>   |- (A = B <-> E.x(x = A /\ x = B))
Theorem	alexeq 2390	Two ways to express substitution of A for x in ph.
|- A e. _V   =>   |- (A.x(x = A -> ph) <-> E.x(x = A /\ ph))
Theorem	ceqex 2391	Equality implies equivalence with substitution.
|- (x = A -> (ph <-> E.x(x = A /\ ph)))
Theorem	ceqsexg 2392	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 -> (E.x(x = A /\ ph) <-> ps))
Theorem	ceqsexgv 2393	Elimination of an existential quantifier, using implicit substitution.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (E.x(x = A /\ ph) <-> ps))
Theorem	ceqsrexv 2394	Elimination of a restricted existential quantifier, using implicit substitution.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (E.x e. B (x = A /\ ph) <-> ps))
Theorem	ceqsrex2v 2395	Elimination of a restricted existential quantifier, using implicit substitution.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- ((A e. C /\ B e. D) -> (E.x e. C E.y e. D ((x = A /\ y = B) /\ ph) <-> ch))
Theorem	clel2 2396	An alternate definition of class membership when the class is a set.
|- A e. _V   =>   |- (A e. B <-> A.x(x = A -> x e. B))
Theorem	clel3g 2397	An alternate definition of class membership when the class is a set.
|- (B e. C -> (A e. B <-> E.x(x = B /\ A e. x)))
Theorem	clel3 2398	An alternate definition of class membership when the class is a set.
|- B e. _V   =>   |- (A e. B <-> E.x(x = B /\ A e. x))
Theorem	clel4 2399	An alternate definition of class membership when the class is a set.
|- B e. _V   =>   |- (A e. B <-> A.x(x = B -> A e. x))
Theorem	elabgt 2400	Membership in a class abstraction, using implicit substitition. (Closed theorem version of elabg 2405.) (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- ((A e. B /\ A.x(x = A -> (ph <-> ps))) -> (A e. {x | ph} <-> ps))