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-10682

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

Type	Label	Description
Statement
Theorem	rabbii 1801	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 1802	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 1803	Equivalent wff's yield equal restricted class abstractions (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> {x e. A | ps} = {x e. A | ch})
Theorem	rabeqf 1804	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 1805	Equality theorem for restricted class abstractions.
|- (A = B -> {x e. A | ph} = {x e. B | ph})
Theorem	rabeq2i 1806	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 1807	Extend class notation to include the universal class symbol.
class V
Definition	df-v 1808	Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21.
|- V = {x | x = x}
Theorem	visset 1809	All set variables are sets (see isset 1810). Theorem 6.8 of [Quine] p. 43.
|- x e. V
Theorem	isset 1810	Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 1808) 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 2869. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 2870, 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."
|- (A e. V <-> E.x x = A)
Theorem	isseti 1811	A way to say "A is a set" (inference rule).
|- A e. V   =>   |- E.x x = A
Theorem	issetri 1812	A way to say "A is a set" (inference rule).
|- E.x x = A   =>   |- A e. V
Theorem	elisset 1813	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 1814	If a class is a member of another class, it is a set.
|- A e. B   =>   |- A e. V
Theorem	elex 1815	An element of a class exists.
|- (A e. B -> E.x x = A)
Theorem	ralv 1816	A universal quantifier restricted to the universe is unrestricted.
|- (A.x e. V ph <-> A.xph)
Theorem	rexv 1817	An existential quantifier restricted to the universe is unrestricted.
|- (E.x e. V ph <-> E.xph)
Theorem	rabab 1818	A class abstraction restricted to the universe is unrestricted.
|- {x e. V | ph} = {x | ph}
Theorem	ralcom4 1819	Commutation of restricted and unrestricted universal quantifiers.
|- (A.x e. A A.yph <-> A.yA.x e. A ph)
Theorem	rexcom4 1820	Commutation of restricted and unrestricted existential quantifiers.
|- (E.x e. A E.yph <-> E.yE.x e. A ph)
Theorem	ceqsalg 1821	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 1822	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 1823	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 1824	Implicit substitution for class with embedded variable.
|- (th <-> E.x(ch /\ A = B))   &   |- (A = B -> (ph <-> ps))   &   |- (ch -> ph)   =>   |- (th -> ps)
Theorem	2gencl 1825	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 1826	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 1827	Implicit substitution inference for general classes.
|- (x = A -> ch)   &   |- (ch -> (ph <-> ps))   =>   |- (A e. B -> (E.x(ch /\ ph) <-> ps))
Theorem	cgsex2g 1828	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 1829	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 1830	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 1831	Elimination of an existential quantifier, using implicit substitution.
|- A e. V   &   |- (x = A -> (ph <-> ps))   =>   |- (E.x(x = A /\ ph) <-> ps)
Theorem	ceqsex2 1832	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 1833	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 1834	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 1835	Restatement of gencbvex 1834 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 1836	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 1837	Implicit substitution of a class for a set variable. This is a generalization of chvar 1165.
|- (ps -> A.xps)   &   |- A e. V   &   |- (x = A -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl 1838	Implicit substitution of a class for a set variable.
|- A e. V   &   |- (x = A -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl2 1839	Implicit substitution of classes for set variables.
|- A e. V   &   |- B e. V   &   |- ((x = A /\ y = B) -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl3 1840	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 1841	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 1842	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 1843	Implicit substitution of a class for a set variable.
|- (x = A -> (ph <-> ps))   &   |- ph   =>   |- (A e. B -> ps)
Theorem	vtoclbg 1844	Implicit substitution of a class for a set variable.
|- (x = A -> (ph <-> ch))   &