mmtheorems20 - 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 - 1901-2000 - Page 20 of 123

Type	Label	Description
Statement
Theorem	vtocleg 1901	Implicit substitution of a class for a set variable.
|- (x = A -> ph)   =>   |- (A e. B -> ph)
Theorem	vtoclegft 1902	Implicit substitution of a class for a set variable. (Closed theorem version of vtoclef 1903.)
|- ((A e. B /\ A.x(ph -> A.xph) /\ A.x(x = A -> ph)) -> ph)
Theorem	vtoclef 1903	Implicit substitution of a class for a set variable.
|- (ph -> A.xph)   &   |- A e. V   &   |- (x = A -> ph)   =>   |- ph
Theorem	vtocle 1904	Implicit substitution of a class for a set variable.
|- A e. V   &   |- (x = A -> ph)   =>   |- ph
Theorem	vtoclri 1905	Implicit substitution of a class for a set variable.
|- (x = A -> (ph <-> ps))   &   |- A.x e. B ph   =>   |- (A e. B -> ps)
Theorem	cla4gf 1906	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	cla4egf 1907	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	cla4gv 1908	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 1909	Existential specialization, using implicit substitition.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (ps -> E.xph))
Theorem	cla42egv 1910	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 1911	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 1912	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 1913	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 1914	Rule of specialization, using implicit substitition.
|- A e. V   &   |- (x = A -> (ph <-> ps))   =>   |- (A.xph -> ps)
Theorem	cla4ev 1915	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 1916	Existential specialization, using implicit substitition.
|- A e. V   &   |- B e. V   &   |- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- (ps -> E.xE.yph)
Theorem	rcla4 1917	Restricted specialization, using implicit substitition.
|- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A.x e. B ph -> ps))
Theorem	rcla4e 1918	Restricted existential specialization, using implicit substitition.
|- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- ((A e. B /\ ps) -> E.x e. B ph)
Theorem	rcla4v 1919	Restricted specialization, using implicit substitition.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A.x e. B ph -> ps))
Theorem	rcla4cv 1920	Restricted specialization, using implicit substitition.
|- (x = A -> (ph <-> ps))   =>   |- (A.x e. B ph -> (A e. B -> ps))
Theorem	rcla4va 1921	Restricted specialization, using implicit substitition.
|- (x = A -> (ph <-> ps))   =>   |- ((A e. B /\ A.x e. B ph) -> ps)
Theorem	rcla4cva 1922	Restricted specialization, using implicit substitition.
|- (x = A -> (ph <-> ps))   =>   |- ((A.x e. B ph /\ A e. B) -> ps)
Theorem	rcla4ev 1923	Restricted existential specialization, using implicit substitition.
|- (x = A -> (ph <-> ps))   =>   |- ((A e. B /\ ps) -> E.x e. B ph)
Theorem	rcla4dv 1924	Restricted specialization, using implicit substitition.
|- ((ph /\ x = A) -> (ps <-> ch))   =>   |- ((ph /\ A e. B) -> (A.x e. B ps -> ch))
Theorem	rcla4edv 1925	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 1926	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 1927	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 1928	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 1929	A variable introduction law for class equality.
|- A e. V   =>   |- (A = B <-> E.x(x = A /\ x = B))
Theorem	eqvincf 1930	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 1931	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 1932	Equality implies equivalence with substitution.
|- (x = A -> (ph <-> E.x(x = A /\ ph)))
Theorem	ceqsexg 1933	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 1934	Elimination of an existential quantifier, using implicit substitution.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (E.x(x = A /\ ph) <-> ps))
Theorem	ceqsrexv 1935	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 1936	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 1937	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 1938	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 1939	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 1940	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 1941	Membership in a class abstraction, using implicit substitition. (Closed theorem version of elabg 1945.)
|- ((A e. B /\ A.x(x = A -> (ph <-> ps))) -> (A e. {x | ph} <-> ps))
Theorem	elabf 1942	Membership in a class abstraction, using implicit substitition.
|- (ps -> A.xps)   &   |- A e. V   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. {x | ph} <-> ps)
Theorem	elab 1943	Membership in a class abstraction, using implicit substitition. Compare Theorem 6.13 of [Quine] p. 44.
|- A e. V   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. {x | ph} <-> ps)
Theorem	elabgf 1944	Membership in a class abstraction, using implicit substitition. Compare Theorem 6.13 of [Quine] p. 44. This version has bound-variable hypotheses in place of distinct variable restrictions.
|- (y e. A -> A.x y e. A)   &   |- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A e. {x | ph} <-> ps))
Theorem	elabg 1945	Membership in a class abstraction, using implicit substitition. Compare Theorem 6.13 of [Quine] p. 44.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A e. {x | ph} <-> ps))
Theorem	elab2g 1946	Membership in a class abstraction, using implicit substitution.
|- (x = A -> (ph <-> ps))   &   |- B = {x | ph}   =>   |- (A e. C -> (A e. B <-> ps))
Theorem	elab2 1947	Membership in a class abstraction, using implicit substitution.
|- A e. V   &   |- (x = A -> (ph <-> ps))   &   |- B = {x | ph}   =>   |- (A e. B <-> ps)
Theorem	elab3g 1948	Membership in a class abstraction, with a weaker antecedent than elabg 1945.
|- (x = A -> (ph <-> ps))   =>   |- ((ps -> A e. B) -> (A e. {x | ph} <-> ps))
Theorem	elab3 1949	Membership in a class abstraction using implicit substitution.
|- (ps -> A e. V)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. {x | ph} <-> ps)
Theorem	elrabf 1950	Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   &   |- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. {x e. B | ph} <-> (A e. B /\ ps))
Theorem	elrab 1951	Membership in a restricted class abstraction, using implicit substitution.
|- (x = A -> (ph <-> ps))   =>   |- (A e. {x e. B | ph} <-> (A e. B /\ ps))
Theorem	elrab3 1952	Membership in a restricted class abstraction, using implicit substitution.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A e. {x e. B | ph} <-> ps))
Theorem	elrab2 1953	Membership in a class abstraction, using implicit substitution.
|- (x = A -> (ph <-> ps))   &   |- C = {x e. B | ph}   =>   |- (A e. C <-> (A e. B /\ ps))
Theorem	cbvab 1954	Rule used to change bound variables, using implicit substitution.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- {x | ph} = {y | ps}
Theorem	cbvabv 1955	Rule used to change bound variables, using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- {x | ph} = {y | ps}
Theorem	cbvrab 1956	Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions.
|- (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))   =>   |- {x e. A | ph} = {y e. A | ps}
Theorem	cbvrabv 1957	Rule to change the bound variable in a restricted class abstraction, using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- {x e. A | ph} = {y e. A | ps}
Theorem	abidhb 1958	Identity used to create closed-form versions of bound-variable hypothesis builders for class expressions.
|- (A.y(y e. A -> A.x y e. A) -> {z | A.x z e. A} = A)
Theorem	hbeqd 1959	Deduction version of bound-variable hypothesis builder hbeq 1608.
|- (ph -> A.xph)   &   |- (ph -> (y e. A -> A.x y e. A))   &   |- (ph -> (y e. B -> A.x y e. B))   =>   |- (ph -> (A = B -> A.x A = B))
Theorem	hbeld 1960	Deduction version of bound-variable hypothesis builder hbel 1609.
|- (ph -> A.xph)   &   |- (ph -> (y e. A -> A.x y e. A))   &   |- (ph -> (y e. B -> A.x y e. B))   =>   |- (ph -> (A e. B -> A.x A e. B))
Theorem	dedhb 1961	A deduction theorem for converting the inference |- (y e. A -> A.xy e. A) => |- ph into a closed theorem. Use hba1 1039 and hbab 1509 to eliminate the hypothesis of the substitution instance ps of the inference. For converting the inference form into a deduction form, abidhb 1958 is useful.
|- (A = {z | A.x z e. A} -> (ph <-> ps))   &   |- ps   =>   |- (A.y(y e. A -> A.x y e. A) -> ph)
Theorem	eueq 1962	Equality has existential uniqueness.
|- (A e. V <-> E!x x = A)
Theorem	eueq1 1963	Equality has existential uniqueness.
|- A e. V   =>   |- E!x x = A
Theorem	eueq2 1964	Equality has existential uniqueness (split into 2 cases).
|- A e. V   &   |- B e. V   =>   |- E!x((ph /\ x = A) \/ (-. ph /\ x = B))
Theorem	eueq3 1965	Equality has existential uniqueness (split into 3 cases).
|- A e. V   &   |- B e. V   &   |- C e. V   &   |- -. (ph /\ ps)   =>   |- E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))
Theorem	moeq 1966	There is at most one set equal to a class.
|- E*x x = A
Theorem	moeq3 1967	"At most one" property of equality (split into 3 cases). (The first 2 hypotheses could be eliminated with longer proof.)
|- B e. V   &   |- C e. V   &   |- -. (ph /\ ps)   =>   |- E*x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))
Theorem	mosub 1968	"At most one" remains true after substitution.
|- E*xph   =>   |- E*xE.y(y = A /\ ph)
Theorem	mo2icl 1969	Theorem for inferring "at most one."
|- (A.x(ph -> x = A) -> E*xph)
Theorem	moi2 1970	Consequence of "at most one."
|- (x = A -> (ph <-> ps))   =>   |- (((A e. B /\ E*xph) /\ (ph /\ ps)) -> x = A)
Theorem	moi 1971	Equality implied by "at most one."
|- (x = A -> (ph <-> ps))   &   |- (x = B -> (ph <-> ch))   =>   |- (((A e. C /\ B e. D) /\ E*xph /\ (ps /\ ch)) -> A = B)
Theorem	euxfr2 1972	Transfer existential uniqueness from a variable x to another variable y contained in expression A.
|- A e. V   &   |- E*y x = A   =>   |- (E!xE.y(x = A /\ ph) <-> E!yph)
Theorem	euxfr 1973	Transfer existential uniqueness from a variable x to another variable y contained in expression A.
|- A e. V   &   |- E!y x = A   &   |- (x = A -> (ph <-> ps))   =>   |- (E!xph <-> E!yps)
Theorem	reurex 1974	Restricted unique existence implies restricted existence.
|- (E!x e. A ph -> E.x e. A ph)
Theorem	reu5 1975	Restricted uniqueness in terms of "at most one."
|- (E!x e. A ph <-> (E.x e. A ph /\ E*x(x e. A /\ ph)))
Theorem	reu2 1976	A way to express restricted uniqueness.
|- (E!x e. A ph <-> (E.x e. A ph /\ A.x e. A A.y e. A ((ph /\ [y / x]ph) -> x = y)))
Theorem	reu3 1977	A way to express restricted uniqueness.
|- (E!x e. A ph <-> E.y e. A A.x e. A (ph <-> x = y))
Theorem	reu6 1978	A way to express restricted uniqueness.
|- (E!x e. A ph <-> (E.x e. A ph /\ E.y e. A A.x e. A (ph -> x = y)))
Theorem	rmo4 1979	Restricted "at most one" using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (E*x(x e. A /\ ph) <-> A.x e. A A.y e. A ((ph /\ ps) -> x = y))
Theorem	reu4 1980	Restricted uniqueness using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (E!x e. A ph <-> (E.x e. A ph /\ A.x e. A A.y e. A ((ph /\ ps) -> x = y)))
Theorem	reu7 1981	Restricted uniqueness using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (E!x e. A ph <-> (E.x e. A ph /\ E.x e. A A.y e. A (ps -> x = y)))
Theorem	reu8 1982	Restricted uniqueness using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (E!x e. A ph <-> E.x e. A (ph /\ A.y e. A (ps -> x = y)))
Theorem	2reuswap 1983	A condition allowing swap of uniqueness and existential quantifiers.
|- (A.x e. A E*y(y e. A /\ ph) -> (E!x e. A E.y e. A ph -> E!y e. A E.x e. A ph))
Russell's Paradox
Theorem	ru 1984	Russell's Paradox. Proposition 4.14 of [TakeutiZaring] p. 14. Frege's Axiom of (unrestricted) Comprehension, expressed in our notation as A e. V, asserted that any collection of sets A is a set i.e. belongs to the universe V of all sets. In particular, by substituting {x | x e/ x} (the "Russell class") for A, it asserted {x | x e/ x} e. V, meaning that the "collection of all sets which are not members of themselves" is a set. However, here we prove {x | x e/ x} e/ V. This contradiction was discovered by Russell in 1901 (published in 1903), invalidating Comprehension and leading to the collapse of Frege's system. In 1908 Zermelo rectified this fatal flaw by replacing Comprehension with a weaker Subset (or Separation) Axiom ssex 2793 asserting that A is a set only when it is smaller than some other set B. However, Zermelo was then faced with a "chicken and egg" problem of how to show B is a set, leading him to introduce the set-building axioms of Null Set 0ex 2785, Pairing prex 2857, Union uniex 3093, Power Set pwex 2823, and Infinity omex 4772 to give him some starting sets to work with (all of which, before Russell's Paradox, were immediate consequences of Frege's Comprehension). In 1922 Fraenkel strengthened the Subset Axiom with our present Replacement Axiom funimaex 3682 (whose modern formalization is due to Skolem, also in 1922). Thus in a very real sense Russell's Paradox spawned the invention of ZF set theory and completely revised the foundations of mathematics! Another mainstream formalization of set theory, devised by von Neumann, Bernays, and Goedel, uses class variables rather than set variables as its primitives. The axiom system NBG in [Mendelson] p. 225 is suitable for a Metamath encoding. NBG is a conservative extension of ZF in that it proves exactly the same theorems as ZF that are expressible in the language of ZF. An advantage of NBG is that it is finitely axiomatizable - the Axiom of Replacement can be broken down into a finite set of formulas that eliminate its wff metavariable. Finite axiomatizability is required by some proof languages (although not by Metamath). There is a stronger version of NBG called Morse-Kelley (axiom system MK in [Mendelson] p. 287). Russell himself continued in a different direction, avoiding the paradox with his "theory of types." Quine extended Russell's ideas to formulate the very strong New Foundations set theory (axiom system NF of [Quine] p. 331). In NF, the collection of all sets is a set, contradicting ZF and NBG set theories, and it has other bizarre consequences: when sets become too huge (beyond the size of those used in standard mathematics), the Axiom of Choice ac4 4896 and Cantor's Theorem canth 4205 are provably false! (See ncanth 4206 for some intuition behind the latter.) Nonetheless, NF has not been shown to be inconsistent and has its advocates - who's to say which set theory is "right"? NF is finitely axiomatizable and can be encoded in Metamath using the axioms from T. Hailperin, "A set of axioms for logic," J. Symb. Logic 9:1-19 (1944). Under our ZF set theory, every set is a member of the Russell class by elirrv 4741 (derived from the Axiom of Regularity), so for us the Russell class equals the universe V (theorem ruv 4744). See ruALT 4745 for an alternate proof of ru 1984 derived from that fact.
|- {x | x e/ x} e/ V
Proper substitution of classes for sets
Theorem	sbhypf 1985	Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf 2080. (Contributed by Raph Levien, 10-Apr-2004.)
|- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- (y = A -> ([y / x]ph <-> ps))
Theorem	sbralie 1986	Implicit to explicit substitution that swaps variables in a quantified expression.
|- (x = y -> (ph <-> ps))   =>   |- ([x / y]A.x e. y ph <-> A.y e. x ps)
Definition	df-sbc 1987	Define the proper substitution of a class for a set. This definition applies to proper classes but is not meaningful in that case (and does not produce the same results as Definition 6.6 of [Quine] p. 42). This definition is somewhat arbitrary in how it behaves with proper classes - e.g., we could have used sbc6 2002, which yields a different result for proper classes. In order to allow for a possible alternate but conflicting definition in the future, we will not commit to any specific proper class behavior. Instead, we will use this definition only to prove dfsbcq 1988, which will in turn serve as the starting point for all theorems based on the definition. Note: this definition extends or "overloads" df-sb 1209 which (via df-clab 1506) becomes a special case of it, so a careful metalogical soundness justification, outside of Metamath, is needed for complete rigor; alternately, we could treat this definition as a new axiom. The related definition df-csb 2052 defines proper substitution into a class variable (as opposed to a wff variable).
|- ([A / x]ph <-> A e. {x | ph})
Theorem	dfsbcq 1988	This theorem, which is similar to Theorem 6.7 of [Quine] p. 42, provides us with a weak definition of the proper substitution of a class for a set, which we will use in place of df-sbc 1987 above. We will derive all our results from starting from here instead of df-sbc 1987. As a consequence, we can derive elabs 2014, which is a weaker version of df-sbc 1987 that leaves substitution undefined when A is a proper class. We thus leave unspecified the "official" behavior for proper classes, which could be as in the sbc5 2001 assertion (always false) or as in sbc6 2002 (always true), or some more meaningful possibility in the future, that some clever person may discover, that is closer to Quine's definition. (Quine's definition has neither behavior for proper classes, and by using dfsbcq 1988 as the definition, we leave it unspecified so as not to conflict. Quine's definition is based on the formula's structure rather than its logical properties and apparently cannot be expressed directly in our formal system.) While in principle we could have made this theorem the official definition, we use df-sbc 1987 because it is more obviously eliminable and thus easier to justify metalogically. But to avoid conflict with Quine, we never use df-sbc 1987 except indirectly via this theorem.
|- (A = B -> ([A / x]ph <-> [B / x]ph))
Theorem	sbceq1a 1989	Equality theorem for class substitution.
|- (x = A -> (ph <-> [A / x]ph))
Theorem	a4sbc 1990	Specialization: if a formula is true for all sets, it is true for any class which is a set. Similar to Theorem 6.11 of [Quine] p. 44. See also stdpc4 1222 and ra4sbc 2047.
|- (A e. B -> (A.xph -> [A / x]ph))
Theorem	sbcth 1991	A substitution into a theorem remains true (when A is a set).
|- ph   =>   |- (A e. B -> [A / x]ph)
Theorem	sbcthdv 1992	Deduction version of sbcth 1991.
|- (ph -> ps)   =>   |- ((ph /\ A e. B) -> [A / x]ps)
Theorem	hbsbc1g 1993	Bound-variable hypothesis builder for class substitution. (The antecedent ensures that A is a set, which is necessary if we restrict ourselves to using only the "weak" class substitution definition dfsbcq 1988.)
|- (y e. A -> A.x y e. A)   =>   |- (A e. B -> ([A / x]ph -> A.x[A / x]ph))
Theorem	hbsbc1 1994	Bound-variable hypothesis builder for class substitution. (The antecedent ensures that A is a set, which is necessary if we restrict ourselves to using only the "weak" class substitution definition dfsbcq 1988.)
|- (y e. A -> A.x y e. A)   =>   |- ((A e. B -> [A / x]ph) -> A.x(A e. B -> [A / x]ph))
Theorem	hbsbc1v 1995	Bound-variable hypothesis builder for class substitution.
|- A e. V   =>   |- ([A / x]ph -> A.x[A / x]ph)
Theorem	hbsbcg 1996	Bound-variable hypothesis builder for class substitution. (The proof was shortened by Eric Schmidt, 17-Jan-2007.)
|- (z e. A -> A.x z e. A)   &   |- (ph -> A.xph)   =>   |- (A e. B -> ([A / y]ph -> A.x[A / y]ph))
Theorem	sbccog 1997	A composition law for class substitution.
|- (A e. B -> ([A / y][y / x]ph <-> [A / x]ph))
Theorem	sbcco2 1998	A composition law for class substitution. Importantly, x may occur free in the class expression substituted for A.
|- (x = y -> A = B)   =>   |- ([x / y][B / x]ph <-> [A / x]ph)
Theorem	sbc5g 1999	An equivalence for class substitution.
|- (A e. B -> ([A / x]ph <-> E.x(x = A /\ ph)))
Theorem	sbc6g 2000	An equivalence for class substitution.
|- (A e. B -> ([A / x]ph <-> A.x(x = A -> ph)))