mmtheorems12 - 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-10691

Statement List for Metamath Proof Explorer - 1101-1200 - Page 12 of 107

Type	Label	Description
Statement
Theorem	nexd 1101	Deduction for generalization rule for negated wff.
⊢ (φ → ∀xφ)    &   ⊢ (φ → ¬ ψ)    ⇒   ⊢ (φ → ¬ ∃xψ)
Theorem	hbim1 1102	A closed form of hbim 1006.
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    ⇒   ⊢ ((φ → ψ) → ∀x(φ → ψ))
Theorem	albid 1103	Formula-building rule for universal quantifier (deduction rule).
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀xψ ↔ ∀xχ))
Theorem	exbid 1104	Formula-building rule for existential quantifier (deduction rule).
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃xψ ↔ ∃xχ))
Theorem	exan 1105	Place a conjunct in the scope of an existential quantifier.
⊢ (∃xφ ⋀ ψ)    ⇒   ⊢ ∃x(φ ⋀ ψ)
Theorem	albi 1106	Split a biconditional and distribute quantifier.
⊢ (∀x(φ ↔ ψ) ↔ (∀x(φ → ψ) ⋀ ∀x(ψ → φ)))
Theorem	2albi 1107	Split a biconditional and distribute 2 quantifiers.
⊢ (∀x∀y(φ ↔ ψ) ↔ (∀x∀y(φ → ψ) ⋀ ∀x∀y(ψ → φ)))
Theorem	hbnd 1108	Deduction form of bound-variable hypothesis builder hbn 1003.
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    ⇒   ⊢ (φ → (¬ ψ → ∀x ¬ ψ))
Theorem	hbimd 1109	Deduction form of bound-variable hypothesis builder hbim 1006.
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    &   ⊢ (φ → (χ → ∀xχ))    ⇒   ⊢ (φ → ((ψ → χ) → ∀x(ψ → χ)))
Theorem	hband 1110	Deduction form of bound-variable hypothesis builder hban 1008.
⊢ (φ → (ψ → ∀xψ))    &   ⊢ (φ → (χ → ∀xχ))    ⇒   ⊢ (φ → ((ψ ⋀ χ) → ∀x(ψ ⋀ χ)))
Theorem	hbbid 1111	Deduction form of bound-variable hypothesis builder hbbi 1009.
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    &   ⊢ (φ → (χ → ∀xχ))    ⇒   ⊢ (φ → ((ψ ↔ χ) → ∀x(ψ ↔ χ)))
Theorem	hbald 1112	Deduction form of bound-variable hypothesis builder hbal 1004.
⊢ (φ → ∀yφ)    &   ⊢ (φ → (ψ → ∀xψ))    ⇒   ⊢ (φ → (∀yψ → ∀x∀yψ))
Theorem	hbexd 1113	Deduction form of bound-variable hypothesis builder hbex 1005.
⊢ (φ → ∀yφ)    &   ⊢ (φ → (ψ → ∀xψ))    ⇒   ⊢ (φ → (∃yψ → ∀x∃yψ))
Theorem	19.21t 1114	Closed form of Theorem 19.21 of [Margaris] p. 90.
⊢ (∀x(φ → ∀xφ) → (∀x(φ → ψ) ↔ (φ → ∀xψ)))
Theorem	19.23t 1115	Closed form of Theorem 19.23 of [Margaris] p. 90.
⊢ (∀x(ψ → ∀xψ) → (∀x(φ → ψ) ↔ (∃xφ → ψ)))
Theorem	exintr 1116	Introduce a conjunct in the scope of an existential quantifier.
⊢ (∀x(φ → ψ) → (∃xφ → ∃x(φ ⋀ ψ)))
Theorem	exintrbi 1117	Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)
⊢ (∀x(φ → ψ) → (∃xφ ↔ ∃x(φ ⋀ ψ)))
Theorem	aaan 1118	Rearrange universal quantifiers.
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ (∀x∀y(φ ⋀ ψ) ↔ (∀xφ ⋀ ∀yψ))
Theorem	eeor 1119	Rearrange existential quantifiers.
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ (∃x∃y(φ ⋁ ψ) ↔ (∃xφ ⋁ ∃yψ))
Theorem	qexmid 1120	Quantified "excluded middle." Exercise 9.2a of Boolos, p. 111, Computability and Logic.
⊢ ∃x(φ → ∀xφ)
Equality
Theorem	ax9o 1121	Show that the original axiom ax-9o 1122 can be derived from ax-9 964 and others. See ax9 1123 for the rederivation of ax-9 964 from ax-9o 1122. This theorem should not be referenced in any proof. Instead, use ax-9o 1122 below so that uses of ax-9o 1122 can be more easily identified.
⊢ (∀x(x = y → ∀xφ) → φ)
Axiom	ax-9o 1122	A variant of ax-9 964. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint). This axiom is redundant, as shown by theorem ax9o 1121.
⊢ (∀x(x = y → ∀xφ) → φ)
Theorem	ax9 1123	Rederivation of axiom ax-9 964 from the orginal version, ax-9o 1122. See ax9o 1121 for the derivation of ax-9o 1122 from ax-9 964. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). This theorem should not be referenced in any proof. Instead, use ax-9 964 above so that uses of ax-9 964 can be more easily identified.
⊢ ¬ ∀x ¬ x = y
Theorem	a9e 1124	At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-5 959 through ax-14 969 and ax-17 970, all axioms other than ax-9 964 are believed to be theorems of free logic, although the system without ax-9 964 is probably not complete in free logic.
⊢ ∃x x = y
Theorem	equid 1125	Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68. This is often an axiom of equality in textbook systems, but we don't need it as an axiom since it can be proved from our other axioms (although the proof, as you can see below, is not as obvious as you might think). This proof uses only axioms without distinct variable conditions and thus requires no dummy variables. A simpler proof, similar to Tarki's, is possible if we make use of ax-17 970; see the proof of equid1 1268.
⊢ x = x
Theorem	stdpc6 1126	One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1179.) Axiom 6 of [Mendelson] p. 95. Mendelson doesn't say why he prepended the redundant quantifier, but it was probably to be compatible with free logic (which is valid in the empty domain).
⊢ ∀x x = x
Theorem	equcomi 1127	Commutative law for equality. Lemma 7 of [Tarski] p. 69.
⊢ (x = y → y = x)
Theorem	equcom 1128	Commutative law for equality.
⊢ (x = y ↔ y = x)
Theorem	equcoms 1129	An inference commuting equality in antecedent. Used to eliminate the need for a syllogism.
⊢ (x = y → φ)    ⇒   ⊢ (y = x → φ)
Theorem	equtr 1130	A transitive law for equality.
⊢ (x = y → (y = z → x = z))
Theorem	equtrr 1131	A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint).
⊢ (x = y → (z = x → z = y))
Theorem	equtr2 1132	A transitive law for equality.
⊢ ((x = z ⋀ y = z) → x = y)
Theorem	equequ1 1133	An equivalence law for equality.
⊢ (x = y → (x = z ↔ y = z))
Theorem	equequ2 1134	An equivalence law for equality.
⊢ (x = y → (z = x ↔ z = y))
Theorem	elequ1 1135	An identity law for the non-logical predicate.
⊢ (x = y → (x ∈ z ↔ y ∈ z))
Theorem	elequ2 1136	An identity law for the non-logical predicate.
⊢ (x = y → (z ∈ x ↔ z ∈ y))
Theorem	ax11i 1137	Inference that has ax-11 966 (without ∀y) as its conclusion and doesn't require ax-10 965, ax-11 966, or ax-12 967 for its proof. The hypotheses may be eliminable without one or more of these axioms in special cases. Proof similar to Lemma 16 of [Tarski] p. 70.
⊢ (x = y → (φ ↔ ψ))    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ (x = y → (φ → ∀x(x = y → φ)))
Axioms ax-10 and ax-11
Theorem	ax10o 1138	Show that ax-10o 1139 can be derived from ax-10 965. An open problem is whether this theorem can be derived from ax-10 965 and the others when ax-11 966 is replaced with ax-11o 1217. See theorem ax10 1140 for the rederivation of ax-10 965 from ax10o 1138. This theorem should not be referenced in any proof. Instead, use ax-10o 1139 below so that uses of ax-10o 1139 can be more easily identified.
⊢ (∀x x = y → (∀xφ → ∀yφ))
Axiom	ax-10o 1139	Axiom ax-10o 1139 ("o" for "old") was the original version of ax-10 965, before it was discovered (in May 2008) that the shorter ax-10 965 could replace it. It appears as Axiom scheme C11' in [Megill] p. 448 (p. 16 of the preprint). This axiom is redundant, as shown by theorem ax10o 1138.
⊢ (∀x x = y → (∀xφ → ∀yφ))
Theorem	ax10 1140	Rederivation of ax-10 965 from original version ax-10o 1139. See theorem ax10o 1138 for the derivation of ax-10o 1139 from ax-10 965. This theorem should not be referenced in any proof. Instead, use ax-10 965 above so that uses of ax-10 965 can be more easily identified.
⊢ (∀x x = y → ∀y y = x)
Theorem	alequcom 1141	Commutation law for identical variable specifiers. The antecedent and consequent are true when x and y are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint).
⊢ (∀x x = y → ∀y y = x)
Theorem	alequcoms 1142	A commutation rule for identical variable specifiers.
⊢ (∀x x = y → φ)    ⇒   ⊢ (∀y y = x → φ)
Theorem	nalequcoms 1143	A commutation rule for distinct variable specifiers.
⊢ (¬ ∀x x = y → φ)    ⇒   ⊢ (¬ ∀y y = x → φ)
Theorem	hbae 1144	All variables are effectively bound in an identical variable specifier.
⊢ (∀x x = y → ∀z∀x x = y)
Theorem	hbaes 1145	Rule that applies hbae 1144 to antecedent.
⊢ (∀z∀x x = y → φ)    ⇒   ⊢ (∀x x = y → φ)
Theorem	hbnae 1146	All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint).
⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
Theorem	hbnaes 1147	Rule that applies hbnae 1146 to antecedent.
⊢ (∀z ¬ ∀x x = y → φ)    ⇒   ⊢ (¬ ∀x x = y → φ)
Theorem	equs3 1148	Lemma used in proofs of substitution properties.
⊢ (∃x(x = y ⋀ φ) ↔ ¬ ∀x(x = y → ¬ φ))
Theorem	equs4 1149	Lemma used in proofs of substitution properties.
⊢ (∀x(x = y → φ) → ∃x(x = y ⋀ φ))
Theorem	equsal 1150	A useful equivalence related to substitution.
⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x(x = y → φ) ↔ ψ)
Theorem	equsex 1151	A useful equivalence related to substitution.
⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃x(x = y ⋀ φ) ↔ ψ)
Theorem	dvelimfALT 1152	Proof of dvelimf 1249 without using ax-11 966. See dvelimALT 1352 for a proof (of the distinct variable version dvelim 1351) that doesn't require ax-10 965.
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀zψ)    &   ⊢ (z = y → (φ ↔ ψ))    ⇒   ⊢ (¬ ∀x x = y → (ψ → ∀xψ))
Theorem	dral1 1153	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).
⊢ (∀x x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x x = y → (∀xφ ↔ ∀yψ))
Theorem	dral2 1154	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).
⊢ (∀x x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x x = y → (∀zφ ↔ ∀zψ))
Theorem	drex1 1155	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).
⊢ (∀x x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x x = y → (∃xφ ↔ ∃yψ))
Theorem	drex2 1156	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).
⊢ (∀x x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x x = y → (∃zφ ↔ ∃zψ))
Theorem	a4imt 1157	Closed theorem form of a4im 1158.
⊢ (∀x((ψ → ∀xψ) ⋀ (x = y → (φ → ψ))) → (∀xφ → ψ))
Theorem	a4im 1158	Specialization with implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The a4im 1158 series of theorems requires that only one direction of the substitution hypothesis hold.
⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ (∀xφ → ψ)
Theorem	a4ime 1159	Existential introduction with implicit substitution. Compare Lemma 14 of [Tarski] p. 70.
⊢ (φ → ∀xφ)    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ (φ → ∃xψ)
Theorem	a4imed 1160	Deduction version of a4ime 1159.
⊢ (χ → ∀xχ)    &   ⊢ (χ → (φ → ∀xφ))    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ (χ → (φ → ∃xψ))
Theorem	cbv1 1161	Rule used to change bound variables with implicit substitution.
⊢ (φ → (ψ → ∀yψ))    &   ⊢ (φ → (χ → ∀xχ))    &   ⊢ (φ → (x = y → (ψ → χ)))    ⇒   ⊢ (∀x∀yφ → (∀xψ → ∀yχ))
Theorem	cbv2 1162	Rule used to change bound variables with implicit substitution.
⊢ (φ → (ψ → ∀yψ))    &   ⊢ (φ → (χ → ∀xχ))    &   ⊢ (φ → (x = y → (ψ ↔ χ)))    ⇒   ⊢ (∀x∀yφ → (∀xψ ↔ ∀yχ))
Theorem	cbv3 1163	Rule used to change bound variables with implicit substitution.
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ (∀xφ → ∀yψ)
Theorem	cbval 1164	Rule used to change bound variables with implicit substitution.
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∀xφ ↔ ∀yψ)
Theorem	cbvex 1165	Rule used to change bound variables with implicit substitution.
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃xφ ↔ ∃yψ)
Theorem	chvar 1166	Implicit substitution of y for x into a theorem. (Contributed by Raph Levien, 9-Jul-2003.)
⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    &   ⊢ φ    ⇒   ⊢ ψ
Theorem	equvini 1167	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109, however we do not require z to be distinct from x and y (making the proof longer).
⊢ (x = y → ∃z(x = z ⋀ z = y))
Theorem	hbequid 1168	Bound-variable hypothesis builder for x = x. This theorem tells us that x is effectively not free in x = x, even though it is technically free according to the traditional definition of free variable. (The proof shows that this can be proved without ax-9 964, even though the theorem equid 1125 cannot be. A shorter proof that uses ax-9 964 is obtainable from equid 1125 and hbth 1000.)
⊢ (x = x → ∀x x = x)
Substitution (without distinct variables)
Syntax	wsbc 1169	Extend wff notation to include the proper substitution of a class for a set. Read this notation as "the proper substitution of class A for set variable x in wff φ." (The purpose of introducing wff [A / x]φ here is to allow us to express i.e. "prove" the wsb 1170 of predicate calculus in terms of the wsbc 1169 of set theory, so that we don't "overload" its connectives with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers. The class variable A is introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus. See df-sbc 1939 for more information on the set theory usage of wsbc 1169.)
wff [A / x]φ
Theorem	wsb 1170	Extend wff definition to include proper substitution (read "the wff that results when y is properly substituted for x in wff φ"). (Instead of introducing wsb 1170 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wsbc 1169. This lets us avoid overloading its connectives, thus preventing ambiguity that would complicate some Metamath parsers. Note: To see the proof steps of this syntax proof, type "show proof wsb /all" in the Metamath program.)
wff [y / x]φ
Definition	df-sb 1171	Define proper substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). For our notation, we use [y / x]φ to mean "the wff that results when y is properly substituted for x in the wff φ." We can also use [y / x]φ in place of the "free for" side condition used in traditional predicate calculus; see, for example, stdpc4 1184. Our notation was introduced in Haskell B. Curry's Foundations of Mathematical Logic (1977), p. 316 and is frequently used in textbooks of lambda calculus and combinatory logic. This notation improves the common but ambiguous notation, "φ(y) is the wff that results when y is properly substituted for x in φ(x)." For example, if the original φ(x) is x = y, then φ(y) is y = y, from which we obtain that φ(x) is x = x. So what exactly does φ(x) mean? Curry's notation solves this problem. In most books, proper substitution has a somewhat complicated recursive definition with multiple cases based on the occurrences of free and bound variables in the wff. Instead, we use a remarkable little formula that is exactly equivalent and gives us a single direct definition. We later prove that our definition has the properties we expect of proper substitution (see theorems sbequ 1228, sbcom2 1333 and sbid2v 1342). Note that our definition is valid even when x and y are replaced with the same variable, as sbid 1183 shows. We achieve this by having x free in the first conjunct and bound in the second. We can also achieve this by using a dummy variable, as the alternate definition dfsb7 1339 shows (which some logicians may prefer because it doesn't mix free and bound variables). Another version that mixes free and bound variables is dfsb3 1225. When x and y are distinct, we can express proper substitution with the simpler expressions of sb5 1267 and sb6 1266. There are no restrictions on any of the variables, including what variables may occur in wff φ.
⊢ ([y / x]φ ↔ ((x = y → φ) ⋀ ∃x(x = y ⋀ φ)))
Theorem	sbimi 1172	Infer substitution into antecedent and consequent of an implication.
⊢ (φ → ψ)    ⇒   ⊢ ([y / x]φ → [y / x]ψ)
Theorem	sbbii 1173	Infer substitution into both sides of a logical equivalence.
⊢ (φ ↔ ψ)    ⇒   ⊢ ([y / x]φ ↔ [y / x]ψ)
Theorem	drsb1 1174	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).
⊢ (∀x x = y → ([z / x]φ ↔ [z / y]φ))
Theorem	sb1 1175	One direction of a simplified definition of substitution.
⊢ ([y / x]φ → ∃x(x = y ⋀ φ))
Theorem	sb2 1176	One direction of a simplified definition of substitution.
⊢ (∀x(x = y → φ) → [y / x]φ)
Theorem	sbequ1 1177	An equality theorem for substitution.
⊢ (x = y → (φ → [y / x]φ))
Theorem	sbequ2 1178	An equality theorem for substitution.
⊢ (x = y → ([y / x]φ → φ))
Theorem	stdpc7 1179	One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 1126.) Translated to traditional notation, it can be read: "x = y → (φ(x, x) → φ(x, y)), provided that y is free for x in φ(x, y)." Axiom 7 of [Mendelson] p. 95.
⊢ (x = y → ([x / y]φ → φ))
Theorem	sbequ12 1180	An equality theorem for substitution.
⊢ (x = y → (φ ↔ [y / x]φ))
Theorem	sbequ12r 1181	An equality theorem for substitution.
⊢ (x = y → ([x / y]φ ↔ φ))
Theorem	sbequ12a 1182	An equality theorem for substitution.
⊢ (x = y → ([y / x]φ ↔ [x / y]φ))
Theorem	sbid 1183	An identity theorem for substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint).
⊢ ([x / x]φ ↔ φ)
Theorem	stdpc4 1184	The specialization axiom of standard predicate calculus. It states that if a statement φ holds for all x, then it also holds for the specific case of y (properly) substituted for x. Translated to traditional notation, it can be read: "∀xφ(x) → φ(y), provided that y is free for x in φ(x)." Axiom 4 of [Mendelson] p. 69. See also a4sbc 1942 and ra4sbc 1994.
⊢ (∀xφ → [y / x]φ)
Theorem	sbf 1185	Substitution for a variable not free in a wff does not affect it.
⊢ (φ → ∀xφ)    ⇒   ⊢ ([y / x]φ ↔ φ)
Theorem	sbf2 1186	Substitution has no effect on a bound variable.
⊢ ([y / x]∀xφ ↔ ∀xφ)
Theorem	sb6x 1187	Equivalence involving substitution for a variable not free.
⊢ (φ → ∀xφ)    ⇒   ⊢ ([y / x]φ ↔ ∀x(x = y → φ))
Theorem	hbs1f 1188	If x is not free in φ, it is not free in [y / x]φ.
⊢ (φ → ∀xφ)    ⇒   ⊢ ([y / x]φ → ∀x[y / x]φ)
Theorem	sbequ5 1189	Substitution does not change an identical variable specifier.
⊢ ([w / z]∀x x = y ↔ ∀x x = y)
Theorem	sbequ6 1190	Substitution does not change a distinctor.
⊢ ([w / z] ¬ ∀x x = y ↔ ¬ ∀x x = y)
Theorem	sbt 1191	A substitution into a theorem remains true. (See chvar 1166 and chvarv 1326 for versions with implicit substitution.
⊢ φ    ⇒   ⊢ [y / x]φ
Theorem	equsb1 1192	Substitution applied to an atomic wff.
⊢ [y / x]x = y
Theorem	equsb2 1193	Substitution applied to an atomic wff.
⊢ [y / x]y = x
Theorem	sbied 1194	Conversion of implicit substitution to explicit substitution (deduction version of sbie 1195).
⊢ (φ → ∀xφ)    &   ⊢ (φ → (χ → ∀xχ))    &   ⊢ (φ → (x = y → (ψ ↔ χ)))    ⇒   ⊢ (φ → ([y / x]ψ ↔ χ))
Theorem	sbie 1195	Conversion of implicit substitution to explicit substitution.
⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ ([y / x]φ ↔ ψ)
Theorems using axiom ax-11
Theorem	equs5a 1196	A property related to substitution that unlike equs5 1220 doesn't require a distinctor antecedent.
⊢ (∃x(x = y ⋀ ∀yφ) → ∀x(x = y → φ))
Theorem	equs5e 1197	A property related to substitution that unlike equs5 1220 doesn't require a distinctor antecedent.
⊢ (∃x(x = y ⋀ φ) → ∀x(x = y → ∃yφ))
Theorem	sb4a 1198	A version of sb4 1222 that doesn't require a distinctor antecedent.
⊢ ([y / x]∀yφ → ∀x(x = y → φ))
Theorem	equs45f 1199	Two ways of expressing substitution when y is not free in φ.
⊢ (φ → ∀yφ)    ⇒   ⊢ (∃x(x = y ⋀ φ) ↔ ∀x(x = y → φ))
Theorem	sb6f 1200	Equivalence for substitution when y is not free in φ.
⊢ (φ → ∀yφ)    ⇒   ⊢ ([y / x]φ ↔ ∀x(x = y → φ))