Metamath Proof Explorer - mmtheorems10

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 - 901-1000 - Page 10 of 58

Type	Label	Description
Statement
Theorem	sbeq2 901	Substitution applied to atomic wff.
|- [y / x]y = x
Theorem	sbequ8 902	Elimination of equality from antecedent after substitution.
|- ([y / x]ph <-> [y / x](x = y -> ph))
Theorem	sbied 903	Conversion of implicit substitution to explicit substitution (deduction version of sbie 904).
|- (ph -> A.xph)   &   |- (ph -> (ch -> A.xch))   &   |- (ph -> (x = y -> (ps <-> ch)))   =>   |- (ph -> ([y / x]ps <-> ch))
Theorem	sbie 904	Conversion of implicit substitution to explicit substitution.
|- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- ([y / x]ph <-> ps)
Theorem	hbsb4 905	A variable not free remains so after substitution with a distinct variable.
|- (ph -> A.zph)   =>   |- (-. A.z z = y -> ([y / x]ph -> A.z[y / x]ph))
Theorem	hbsb4t 906	A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 905).
|- (A.xA.z(ph -> A.zph) -> (-. A.z z = y -> ([y / x]ph -> A.z[y / x]ph)))
Theorem	ddelimf2 907	Proof of ddelimf 908 without using ax-11 801. This may be useful in a study to determine whether ax-11 801 can be derived from the others, which is currently unknown.
|- (ph -> A.xph)   &   |- (ps -> A.zps)   &   |- (z = y -> (ph <-> ps))   =>   |- (-. A.x x = y -> (ps -> A.xps))
Theorem	ddelimf 908	Version of ddelim 1000 without any variable restrictions.
|- (ph -> A.xph)   &   |- (ps -> A.zps)   &   |- (z = y -> (ph <-> ps))   =>   |- (-. A.x x = y -> (ps -> A.xps))
Theorem	ddelimdf 909	Deduction form of ddelimf 908. This version may be useful if we want to avoid ax-17 925 and use ax-16 922 instead.
|- (ph -> A.xph)   &   |- (ph -> A.zph)   &   |- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.zch))   &   |- (ph -> (z = y -> (ps <-> ch)))   =>   |- (ph -> (-. A.x x = y -> (ch -> A.xch)))
Theorem	sbco 910	A composition law for substitution.
|- ([y / x][x / y]ph <-> [y / x]ph)
Theorem	sbid2 911	An identity law for substitution.
|- (ph -> A.xph)   =>   |- ([y / x][x / y]ph <-> ph)
Theorem	sbidm 912	An idempotent law for substitution.
|- ([y / x][y / x]ph <-> [y / x]ph)
Theorem	sbco2 913	A composition law for substitution.
|- (ph -> A.zph)   =>   |- ([y / z][z / x]ph <-> [y / x]ph)
Theorem	sbco2d 914	A composition law for substitution.
|- (ph -> A.xph)   &   |- (ph -> A.zph)   &   |- (ph -> (ps -> A.zps))   =>   |- (ph -> ([y / z][z / x]ps <-> [y / x]ps))
Theorem	sbco3 915	A composition law for substitution.
|- ([z / y][y / x]ph <-> [z / x][x / y]ph)
Theorem	sbcom 916	A commutativity law for substitution.
|- ([y / z][y / x]ph <-> [y / x][y / z]ph)
Theorem	sb5f1 917	Equivalence for substitution. Similar to Theorem 6.2 of [Quine] p. 40.
|- (ph -> A.xph)   =>   |- (ph <-> A.x(x = y -> [x / y]ph))
Theorem	sb8 918	Substitution of variable in universal quantifier.
|- (ph -> A.yph)   =>   |- (A.xph <-> A.y[y / x]ph)
Theorem	sb8e 919	Substitution of variable in existential quantifier.
|- (ph -> A.yph)   =>   |- (E.xph <-> E.y[y / x]ph)
Theorem	sb9i 920	Commutation of quantification and substitution variables.
|- (A.x[x / y]ph -> A.y[y / x]ph)
Theorem	sb9 921	Commutation of quantification and substitution variables.
|- (A.x[x / y]ph <-> A.y[y / x]ph)
Axiom	ax-16 922	Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-17 925 below to be a metatheorem and not an axiom). Axiom scheme C16' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases. It is a somewhat bizarre axiom since the antecedent is always false in set theory (see dtru 1889) but nonetheless technically necessary as you can see from its uses.
|- (A.x x = y -> (ph -> A.xph))
Theorem	ax17eq 923	Theorem to add distinct quantifier to atomic formula.
|- (x = y -> A.z x = y)
Theorem	ax17el 924	Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-17 925 considered as a metatheorem. Do not use it for later proofs - use ax-17 925 instead, to avoid reference to the redundant ax-15 806.)
|- (x e. y -> A.z x e. y)
Axiom	ax-17 925	Axiom to quantify a variable over a formula in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski] p. 77. If we allow ax-15 806 (not otherwise used in our development), this axiom is logically redundant since it is a metatheorem justified by induction on the number of primitive connectives in wff ph, using ax17eq 923 and ax17el 924 together hbne 699, hbal 700, and hbim 702. However if we omit this axiom our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom is effectively a definition of the concept of a set variable not occurring in a wff (as opposed to just two set variables being distinct).
|- (ph -> A.xph)
Theorem	ax11a 926	This is a version of ax-11 801 when the variables are distinct. Axiom (C8) of [Monk2] p. 105.
|- (x = y -> (ph -> A.x(x = y -> ph)))
Theorem	a4b 927	A weaker version of a4a 842.
|- (x = y -> (ph -> ps))   =>   |- (A.xph -> ps)
Theorem	a4b1 928	Infer specialization rule from substitution instance.
|- (x = y -> (ph <-> ps))   =>   |- (A.xph -> ps)
Theorem	a4w 929	A weaker version of a4c 843.
|- (x = y -> (ph -> ps))   =>   |- (ph -> E.xps)
Theorem	a4w1 930	Infer existence from a substitution instance.
|- (x = y -> (ph <-> ps))   &   |- ps   =>   |- E.xph
Theorem	eqvin.l2 931	A variable elimination law for equality. Lemma 15 of [Monk2] p. 109.
|- (E.z(x = z /\ z = y) -> x = y)
Theorem	eqvin 932	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109.
|- (x = y <-> E.z(x = z /\ z = y))
Theorem	a16g 933	A generalization of axiom ax-16 922.
|- (A.x x = y -> (ph -> A.zph))
Theorem	a16gb 934	A generalization of axiom ax-16 922.
|- (A.x x = y -> (ph <-> A.zph))
Theorem	bialdv 935	Formula-building rule for universal quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (A.xps <-> A.xch))
Theorem	biexdv 936	Formula-building rule for existential quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xps <-> E.xch))
Theorem	bi2aldv 937	Formula-building rule for 2 existential quantifiers (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (A.xA.yps <-> A.xA.ych))
Theorem	bi2exdv 938	Formula-building rule for 2 existential quantifiers (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xE.yps <-> E.xE.ych))
Theorem	bi3exdv 939	Formula-building rule for 3 existential quantifiers (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xE.yE.zps <-> E.xE.yE.zch))
Theorem	bi4exdv 940	Formula-building rule for 4 existential quantifiers (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xE.yE.zE.wps <-> E.xE.yE.zE.wch))
Theorem	19.9rv 941	Special case of Theorem 19.9 of [Margaris] p. 89.
|- (ph <-> E.xph)
Theorem	19.21v 942	Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as (ph -> A.xph) in 19.21 738 via the use of distinct variable conditions combined with ax-17 925. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g. euf 1011 derived from df-eu 1009. The "f" stands for "not free in" which is less restrictive than "does not occur in".
|- (A.x(ph -> ps) <-> (ph -> A.xps))
Theorem	19.21aiv 943	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> ps)   =>   |- (ph -> A.xps)
Theorem	19.21aivv 944	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> ps)   =>   |- (ph -> A.xA.yps)
Theorem	19.21adv 945	Deduction from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> A.xch))
Theorem	19.20dv 946	Deduction from Theorem 19.20 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (A.xps -> A.xch))
Theorem	19.22dv 947	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> E.xch))
Theorem	19.20dvv 948	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (A.xA.yps -> A.xA.ych))
Theorem	19.22dvv 949	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (E.xE.yps -> E.xE.ych))
Theorem	19.23v 950	Special case of Theorem 19.23 of [Margaris] p. 90.
|- (A.x(ph -> ps) <-> (E.xph -> ps))
Theorem	19.23vv 951	Theorem 19.23 of [Margaris] p. 90 extended to two variables.
|- (A.xA.y(ph -> ps) <-> (E.xE.yph -> ps))
Theorem	19.23aiv 952	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (ph -> ps)   =>   |- (E.xph -> ps)
Theorem	19.23aivv 953	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (ph -> ps)   =>   |- (E.xE.yph -> ps)
Theorem	19.23adv 954	Deduction from Theorem 19.23 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> ch))
Theorem	19.23advv 955	Deduction from Theorem 19.23 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (E.xE.yps -> ch))
Theorem	19.27v 956	Theorem 19.27 of [Margaris] p. 90.
|- (A.x(ph /\ ps) <-> (A.xph /\ ps))
Theorem	19.28v 957	Theorem 19.28 of [Margaris] p. 90.
|- (A.x(ph /\ ps) <-> (ph /\ A.xps))
Theorem	19.36v 958	Special case of Theorem 19.36 of [Margaris] p. 90.
|- (E.x(ph -> ps) <-> (A.xph -> ps))
Theorem	19.36aiv 959	Inference from Theorem 19.36 of [Margaris] p. 90.
|- E.x(ph -> ps)   =>   |- (A.xph -> ps)
Theorem	19.12vv 960	Special case of 19.12 729 where its converse holds.
|- (E.xA.y(ph -> ps) <-> A.yE.x(ph -> ps))
Theorem	19.37v 961	Special case of Theorem 19.37 of [Margaris] p. 90.
|- (E.x(ph -> ps) <-> (ph -> E.xps))
Theorem	19.37aiv 962	Inference from Theorem 19.37 of [Margaris] p. 90.
|- E.x(ph -> ps)   =>   |- (ph -> E.xps)
Theorem	19.41v 963	Special case of Theorem 19.41 of [Margaris] p. 90.
|- (E.x(ph /\ ps) <-> (E.xph