mmtheorems23 - 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 - 2201-2300 - Page 23 of 175

Type	Label	Description
Statement
Theorem	reximdvai 2201	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
|- (ph -> (x e. A -> (ps -> ch)))   =>   |- (ph -> (E.x e. A ps -> E.x e. A ch))
Theorem	reximdv 2202	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.)
|- (ph -> (ps -> ch))   =>   |- (ph -> (E.x e. A ps -> E.x e. A ch))
Theorem	reximdva 2203	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
|- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (E.x e. A ps -> E.x e. A ch))
Theorem	r19.12 2204	Theorem 19.12 of [Margaris] p. 89 with restricted quantifiers. (The proof was shortened by Andrew Salmon, 30-May-2011.)
|- (E.x e. A A.y e. B ph -> A.y e. B E.x e. A ph)
Theorem	r19.12OLD 2205	Theorem 19.12 of [Margaris] p. 89 with restricted quantifiers.
|- (E.x e. A A.y e. B ph -> A.y e. B E.x e. A ph)
Theorem	r19.23 2206	Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers.
|- (ps -> A.xps)   =>   |- (A.x e. A (ph -> ps) <-> (E.x e. A ph -> ps))
Theorem	r19.23OLD 2207	Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers.
|- (ps -> A.xps)   =>   |- (A.x e. A (ph -> ps) <-> (E.x e. A ph -> ps))
Theorem	r19.23v 2208	Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers.
|- (A.x e. A (ph -> ps) <-> (E.x e. A ph -> ps))
Theorem	r19.23ai 2209	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (The proof was shortened by Andrew Salmon, 30-May-2011.)
|- (ps -> A.xps)   &   |- (x e. A -> (ph -> ps))   =>   |- (E.x e. A ph -> ps)
Theorem	r19.23aiOLD 2210	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ps -> A.xps)   &   |- (x e. A -> (ph -> ps))   =>   |- (E.x e. A ph -> ps)
Theorem	r19.23aiv 2211	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.)
|- (x e. A -> (ph -> ps))   =>   |- (E.x e. A ph -> ps)
Theorem	r19.23aiva 2212	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).
|- ((x e. A /\ ph) -> ps)   =>   |- (E.x e. A ph -> ps)
Theorem	r19.23ad 2213	Deduction from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (The proof was shortened by Andrew Salmon, 30-May-2011.)
|- (ph -> A.xph)   &   |- (ch -> A.xch)   &   |- (ph -> (x e. A -> (ps -> ch)))   =>   |- (ph -> (E.x e. A ps -> ch))
Theorem	r19.23adOLD 2214	Deduction from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).
|- (ph -> A.xph)   &   |- (ch -> A.xch)   &   |- (ph -> (x e. A -> (ps -> ch)))   =>   |- (ph -> (E.x e. A ps -> ch))
Theorem	r19.23adv 2215	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (The proof was shortened by Eric Schmidt, 22-Dec-2006.)
|- (ph -> (x e. A -> (ps -> ch)))   =>   |- (ph -> (E.x e. A ps -> ch))
Theorem	r19.23adva 2216	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).
|- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (E.x e. A ps -> ch))
Theorem	r19.23aivv 2217	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).
|- ((x e. A /\ y e. B) -> (ph -> ps))   =>   |- (E.x e. A E.y e. B ph -> ps)
Theorem	r19.23advv 2218	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> ((x e. A /\ y e. B) -> (ps -> ch)))   =>   |- (ph -> (E.x e. A E.y e. B ps -> ch))
Theorem	r19.26 2219	Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers. (The proof was shortened by Andrew Salmon, 30-May-2011.)
|- (A.x e. A (ph /\ ps) <-> (A.x e. A ph /\ A.x e. A ps))
Theorem	r19.26OLD 2220	Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers.
|- (A.x e. A (ph /\ ps) <-> (A.x e. A ph /\ A.x e. A ps))
Theorem	r19.26-2 2221	Theorem 19.26 of [Margaris] p. 90 with 2 restricted quantifiers.
|- (A.x e. A A.y e. B (ph /\ ps) <-> (A.x e. A A.y e. B ph /\ A.x e. A A.y e. B ps))
Theorem	r19.26m 2222	Theorem 19.26 of [Margaris] p. 90 with mixed quantifiers.
|- (A.x((x e. A -> ph) /\ (x e. B -> ps)) <-> (A.x e. A ph /\ A.x e. B ps))
Theorem	ralbi 2223	Distribute a restricted universal quantifier over a biconditional. Theorem 19.15 of [Margaris] p. 90 with restricted quantification.
|- (A.x e. A (ph <-> ps) -> (A.x e. A ph <-> A.x e. A ps))
Theorem	r19.27av 2224	Restricted version of one direction of Theorem 19.27 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.) (The proof was shortened by Andrew Salmon, 30-May-2011.)
|- ((A.x e. A ph /\ ps) -> A.x e. A (ph /\ ps))
Theorem	r19.27avOLD 2225	Restricted version of one direction of Theorem 19.27 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.)
|- ((A.x e. A ph /\ ps) -> A.x e. A (ph /\ ps))
Theorem	r19.28av 2226	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 2227	Theorem 19.29 of [Margaris] p. 90 with restricted quantifiers. (The proof was shortened by Andrew Salmon, 30-May-2011.)
|- ((A.x e. A ph /\ E.x e. A ps) -> E.x e. A (ph /\ ps))
Theorem	r19.29OLD 2228	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 2229	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 2230	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 2231	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 2232	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 2233	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 2234	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.41 2235	Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (E.x e. A (ph /\ ps) <-> (E.x e. A ph /\ ps))
Theorem	r19.41v 2236	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 2237	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 2238	Restricted version of Theorem 19.43 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 30-May-2011.)
|- (E.x e. A (ph \/ ps) <-> (E.x e. A ph \/ E.x e. A ps))
Theorem	r19.43OLD 2239	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 2240	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 2241	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	ralcom 2242	Commutation of restricted quantifiers.
|- (A.x e. A A.y e. B ph <-> A.y e. B A.x e. A ph)
Theorem	rexcom 2243	Commutation of restricted quantifiers.
|- (E.x e. A E.y e. B ph <-> E.y e. B E.x e. A ph)
Theorem	ralcom2 2244	Commutation of restricted quantifiers. Note that x and y needn't be distinct (this makes the proof longer but illustrates the use of dvelim 1743). (The proof was shortened by Andrew Salmon, 30-May-2011.)
|- (A.x e. A A.y e. A ph -> A.y e. A A.x e. A ph)
Theorem	ralcom2OLD 2245	Commutation of restricted quantifiers. Note that x and y needn't be distinct (this makes the proof longer but illustrates the use of dvelim 1743).
|- (A.x e. A A.y e. A ph -> A.y e. A A.x e. A ph)
Theorem	ralcom3 2246	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	reean 2247	Rearrange existential quantifiers. (The proof was shortened by Andrew Salmon, 30-May-2011.)
|- (ph -> A.yph)   &   |- (ps -> A.xps)   =>   |- (E.x e. A E.y e. B (ph /\ ps) <-> (E.x e. A ph /\ E.y e. B ps))
Theorem	reeanOLD 2248	Rearrange existential quantifiers.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   =>   |- (E.x e. A E.y e. B (ph /\ ps) <-> (E.x e. A ph /\ E.y e. B ps))
Theorem	reeanv 2249	Rearrange existential quantifiers.
|- (E.x e. A E.y e. B (ph /\ ps) <-> (E.x e. A ph /\ E.y e. B ps))
Theorem	2ralor 2250	Distribute quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010.)
|- (A.x e. A A.y e. B (ph \/ ps) <-> (A.x e. A ph \/ A.y e. B ps))
Theorem	hbreu 2251	Bound-variable hypothesis builder for restricted uniqueness.
|- (y e. A -> A.x y e. A)   &   |- (ph -> A.xph)   =>   |- (E!y e. A ph -> A.xE!y e. A ph)
Theorem	hbreu1 2252	x is not free in E!x e. Aph.
|- (E!x e. A ph -> A.xE!x e. A ph)
Theorem	rabid 2253	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 2254	An "identity" law for restricted class abstraction. (The proof was shortened by Andrew Salmon, 30-May-2011.)
|- (A = {x e. A | ph} <-> A.x e. A ph)
Theorem	rabid2OLD 2255	An "identity" law for restricted class abstraction.
|- (A = {x e. A | ph} <-> A.x e. A ph)
Theorem	rabswap 2256	Swap with a membership relation in a restricted class abstraction.
|- {x e. A | x e. B} = {x e. B | x e. A}
Theorem	hbrab1 2257	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 2258	A variable not free in a wff remains so in a restricted class abstraction. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
|- (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	reubidva 2259	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 2260	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 2261	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 2262	Formula-building rule for restricted existential quantifier (inference rule).
|- (ph <-> ps)   =>   |- (E!x e. A ph <-> E!x e. A ps)
Theorem	raleqf 2263	Equality theorem for restricted universal quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
|- (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	rexeqf 2264	Equality theorem for restricted existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
|- (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 2265	Equality theorem for restricted uniqueness quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
|- (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	raleq 2266	Equality theorem for restricted universal quantifier.
|- (A = B -> (A.x e. A ph <-> A.x e. B ph))
Theorem	rexeq 2267	Equality theorem for restricted existential quantifier.
|- (A = B -> (E.x e. A ph <-> E.x e. B ph))
Theorem	reueq1 2268	Equality theorem for restricted uniqueness quantifier.
|- (A = B -> (E!x e. A ph <-> E!x e. B ph))
Theorem	raleqdv 2269	Equality deduction for restricted universal quantifier.
|- (ph -> A = B)   =>   |- (ph -> (A.x e. A ps <-> A.x e. B ps))
Theorem	rexeqdv 2270	Equality deduction for restricted existential quantifier.
|- (ph -> A = B)   =>   |- (ph -> (E.x e. A ps <-> E.x e. B ps))
Theorem	raleqbi1dv 2271	Equality deduction for restricted universal quantifier.
|- (A = B -> (ph <-> ps))   =>   |- (A = B -> (A.x e. A ph <-> A.x e. B ps))
Theorem	rexeqbi1dv 2272	Equality deduction for restricted existential quantifier.
|- (A = B -> (ph <-> ps))   =>   |- (A = B -> (E.x e. A ph <-> E.x e. B ps))
Theorem	reueqd 2273	Equality deduction for restricted uniqueness quantifier.
|- (A = B -> (ph <-> ps))   =>   |- (A = B -> (E!x e. A ph <-> E!x e. B ps))
Theorem	raleqbidv 2274	Equality deduction for restricted universal quantifier.
|- (ph -> A = B)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. B ch))
Theorem	rexeqbidv 2275	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 2276	Rule used to change bound variables, using implicit substitition. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
|- (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 2277	Rule used to change bound variables, using implicit substitition. (Contributed by FL, 11-Jul-2011.) (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
|- (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 2278	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 2279	Rule used to change bound variables, using implicit substitition. (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (E.x e. A ph <-> E.y e. A ps)
Theorem	cbvralv 2280	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 2281	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 2282	Change the bound variable of a restricted uniqueness quantifier using implicit substitution. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
|- (x = y -> (ph <-> ps))   =>   |- (E!x e. A ph <-> E!y e. A ps)
Theorem	cbvral2v 2283	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 2284	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	rabbiia 2285	Equivalent wff's yield equal restricted class abstractions (inference rule).
|- (x e. A -> (ph <-> ps))   =>   |- {x e. A | ph} = {x e. A | ps}
Theorem	rabbidva 2286	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	rabbidv 2287	Equivalent wff's yield equal restricted class abstractions (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> {x e. A | ps} = {x e. A | ch})
Theorem	rabeqf 2288	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 2289	Equality theorem for restricted class abstractions.
|- (A = B -> {x e. A | ph} = {x e. B | ph})
Theorem	rabeqbidv 2290	Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.)
|- (ph -> A = B)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> {x e. A | ps} = {x e. B | ch})
Theorem	rabeq2i 2291	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 2292	Extend class notation to include the universal class symbol.
class _V
Theorem	vjust 2293	Soundness justification theorem for df-v 2294. (Contributed by Rodolfo Medina, 27-Apr-2010.)
|- {x | x = x} = {y | y = y}
Definition	df-v 2294	Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21.
|- _V = {x | x = x}
Theorem	visset 2295	All set variables are sets (see isset 2296). Theorem 6.8 of [Quine] p. 43.
|- x e. _V
Theorem	isset 2296	Two ways to say "A is a set": A class A is a member of the universal class _V (see df-v 2294) 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 3794. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 3795, 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 1880 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 2297	A way to say "A is a set" (inference rule).
|- A e. _V   =>   |- E.x x = A
Theorem	issetri 2298	A way to say "A is a set" (inference rule).
|- E.x x = A   =>   |- A e. _V
Theorem	elisset 2299	If a class is a member of another class, it is a set. Theorem 6.12 of [Quine] p. 44. (The proof was shortened by Andrew Salmon, 8-Jun-2011.)
|- (A e. B -> A e. _V)
Theorem	elissetOLD 2300	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)