Metamath Proof Explorer - mmtheorems15

Jump to page: 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-5787

Statement List for Metamath Proof Explorer - 1401-1500 - Page 15 of 58

Type	Label	Description
Statement
Theorem	cla4ev 1401	Existential specialization with implicit substitution.
|- A e. V   &   |- (x = A -> (ph <-> ps))   =>   |- (ps -> E.xph)
Theorem	rcla4v 1402	Restricted specialization with implicit substitution.
|- (x = A -> (ph <-> ps))   =>   |- (A.x e. B ph -> (A e. B -> ps))
Theorem	rcla4ev 1403	Restricted existential specialization with implicit substitution.
|- (x = A -> (ph <-> ps))   =>   |- ((A e. B /\ ps) -> E.x e. B ph)
Theorem	rcla42v 1404	2-variable restricted specialization with implicit substitution.
|- (x = A -> (ph <-> ch))   &   |- (y = B -> (ch <-> ps))   =>   |- (A.x e. C A.y e. D ph -> ((A e. C /\ B e. D) -> ps))
Theorem	rcla42ev 1405	2-variable restricted existential specialization with 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	cla4e2v 1406	Existential specialization with implicit substitution.
|- A e. V   &   |- B e. V   &   |- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- (ps -> E.xE.yph)
Theorem	eqvinc 1407	A variable introduction law for class equality.
|- A e. V   =>   |- (A = B <-> E.x(x = A /\ x = B))
Theorem	eqvincf 1408	A variable introduction law for class equality, requiring only that x not be free in A and B (instead of not occurring in them).
|- (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 1409	Two ways of expressing substitution of A for x in ph.
|- A e. V   =>   |- (A.x(x = A -> ph) <-> E.x(x = A /\ ph))
Theorem	ceqex 1410	Equality implies equivalence with substitution.
|- (x = A -> (ph <-> E.x(x = A /\ ph)))
Theorem	ceqsexg 1411	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 1412	Elimination of an existential quantifier, using implicit substitution.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (E.x(x = A /\ ph) <-> ps))
Theorem	ceqsrexv 1413	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	elabf 1414	Membership in a class abstraction with implicit substitution.
|- (ps -> A.xps)   &   |- A e. V   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. {x | ph} <-> ps)
Theorem	elab 1415	Membership in a class abstraction with implicit substitution. Compare Theorem 6.13 of [Quine] p. 44.
|- A e. V   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. {x | ph} <-> ps)
Theorem	elabgf 1416	Membership in a class abstraction with implicit substitution. 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 1417	Membership in a class abstraction with implicit substitution. Compare Theorem 6.13 of [Quine] p. 44.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A e. {x | ph} <-> ps))
Theorem	elab2g 1418	Membership in a class abstraction, using implicit substitution.
|- (x = A -> (ph <-> ps))   &   |- B = {x | ph}   =>   |- (A e. C -> (A e. B <-> ps))
Theorem	elab2 1419	Membership in a class abstraction, using implicit substitution.
|- A e. V   &   |- (x = A -> (ph <-> ps))   &   |- B = {x | ph}   =>   |- (A e. B <-> ps)
Theorem	elab3g 1420	Membership in a class abstraction using implicit substitution.
|- (ps -> A e. V)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. {x | ph} <-> ps)
Theorem	elrabf 1421	Membership in a restricted class abstraction with 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 1422	Membership in a restricted class abstraction with implicit substitution.
|- (x = A -> (ph <-> ps))   =>   |- (A e. {x e. B | ph} <-> (A e. B /\ ps))
Theorem	cbvab 1423	Rule used to change bound variables with implicit substitution.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- {x | ph} = {y | ps}
Theorem	cbvabv 1424	Rule used to change bound variables with implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- {x | ph} = {y | ps}
Theorem	cbvrab 1425	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 1426	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	eueq 1427	Equality has existential uniqueness.
|- (A e. V <-> E!x x = A)
Theorem	eueq1 1428	Equality has existential uniqueness.
|- A e. V   =>   |- E!x x = A
Theorem	eueq2 1429	Equality has existential uniqueness (split into 2 cases).
|- A e. V   &   |- B e. V   =>   |- E!x((ph /\ x = A) \/ (-. ph /\ x = B))
Theorem	eueq3 1430	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 1431	There is at most one set equal to a class.
|- E*x x = A
Theorem	moeq3 1432	"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 1433	"At most one" remains true after substitution.
|- E*xph   =>   |- E*xE.y(y = A /\ ph)
Theorem	mo2icl 1434	Theorem for inferring "at most one".
|- (A.x(ph -> x = A) -> E*xph)
Theorem	euxfr2 1435	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 1436	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	ru 1437	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} 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 1700 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 1745, Pairing prex 1892, Union uniex 1947, Power Set pwex 1806, and Infinity omex 3475 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 2716 (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 set 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 3571 and Cantor's Theorem canth2 3381 are provably false! 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).
|- {x | x e/ x} e/ V
Theorem	vsbcint 1438	Change variable of an implicit substitution hypothesis, introducing an explicit substitution. (Contributed by Raph Levien, 10-Apr-04.)
|- (x = A -> (ph <-> ps))   =>   |- (y = A -> ([y / x]ph <-> ps))
Theorem	sbralie 1439	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)
Syntax	wsbc 1440	Extend wff notation to include the proper substitution of a class for a set. This definition "overloads" the previously defined variable substitution wsb 852 (where the first argument is a set variable rather than a class variable). We take care to ensure that this new definition is a conservative extension. Read this notation as "the proper substitution of class A for set variable x in wff ph".
wff [A / x]ph
Definition	df-sbc 1441	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 - e.g., we could have used sbc6 1453 which yields a different result for proper classes. In order to allow for a possible alternate but conflicting definition in the future, we will use this definition only to prove dfsbcq 1442, which will then in turn serve as our "real" definition. Note: this definition extends or "overloads" df-sb 853 which ( via df-clab 1093) becomes a special case of it. Theorem sbab 1188 shows how proper substitution into a class variable (as opposed to a wff) could be defined. (We do not have a separate notation for it at this time.)
|- ([A / x]ph <-> A e. {x | ph})
Theorem	dfsbcq 1442	This theorem, which is similar to Theorem 6.7 of [Quine] p. 42, provides us a weak definition of the proper substitution of a class for a set that we will use in place of df-sbc 1441 above. We derive all our results from starting from here instead of df-sbc 1441; in particular, substitution will become undefined when A or B is a proper class. This will leave unspecified the "official" behavior for proper classes, which could be as in the sbc5 1452 assertion (always false) or as in sbc6 1453 (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 actual definition cannot be expressed simply in our formal system.)
|- (A = B -> ([A / x]ph <-> [B / x]ph))
Theorem	sbceq1 1443	Equality theorem for class substitution.
|- (x = A -> (ph <-> [A / x]ph))
Theorem	a4sbc 1444	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.
|- (A e. B -> (A.xph -> [A / x]ph))
Theorem	hbsbcg 1445	Bound variable hypothesis builder for class substitution.
|- (y e. A -> A.x y e. A)   =>   |- (A e. B -> ([A / x]ph -> A.x[A / x]ph))
Theorem	hbsbc 1446	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 1442.)
|- (y e. A -> A.x y e. A)   =>   |- ((A e. B -> [A / x]ph) -> A.x(A e. B -> [A / x]ph))
Theorem	hbsbcv 1447	Bound variable hypothesis builder for class substitution.
|- A e. V   =>   |- ([A / x]ph -> A.x[A / x]ph)
Theorem	sbcco 1448	A composition law for class substitution.
|- (A e. B -> ([A / y][y / x]ph <-> [