![]() |
Metamath
Proof Explorer Theorem List (p. 25 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | spei 2401 | Inference from existential specialization, using implicit substitution. Remove a distinct variable constraint. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker speiv 1976 if possible. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ ∃𝑥𝜑 | ||
Theorem | chvar 2402 | Implicit substitution of 𝑦 for 𝑥 into a theorem. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker chvarfv 2240 if possible. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | chvarv 2403* | Implicit substitution of 𝑦 for 𝑥 into a theorem. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker chvarvv 2005 if possible. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | cbv3 2404 | Rule used to change bound variables, using implicit substitution, that does not use ax-c9 36186. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker cbv3v 2344 if possible. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbval 2405 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. Check out cbvalw 2042, cbvalvw 2043, cbvalv1 2350 for versions requiring fewer axioms. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvex 2406 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. Check out cbvexvw 2044, cbvexv1 2351 for weaker versions requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbvalv 2407* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. See cbvalvw 2043 for a version requiring fewer axioms, to be preferred when sufficient. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2142, shorten. (Revised by Wolf Lammen, 11-Sep-2023.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvexv 2408* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. See cbvexvw 2044 for a version requiring fewer axioms, to be preferred when sufficient. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-10 2142, shorten. (Revised by Wolf Lammen, 11-Sep-2023.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbvalvOLD 2409* | Obsolete version of cbvalv 2407 as of 11-Sep-2023. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2142. (Revised by Wolf Lammen, 17-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvexvOLD 2410* | Obsolete version of cbvexv 2408 as of 11-Sep-2023. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-10 2142. (Revised by Wolf Lammen, 17-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbv1 2411 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. See cbv1v 2345 with disjoint variable conditions, not depending on ax-13 2379. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | cbv2 2412 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. See cbv2w 2346 with disjoint variable conditions, not depending on ax-13 2379. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style, avoid ax-10 2142. (Revised by Wolf Lammen, 10-Sep-2023.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbv3h 2413 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker cbv3hv 2349 if possible. (Contributed by NM, 8-Jun-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbv1h 2414 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 13-May-2018.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | cbv2h 2415 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 11-May-1993.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbv2OLD 2416 | Obsolete version of cbv2 2412 as of 10-Sep-2023. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvald 2417* | Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2462. Usage of this theorem is discouraged because it depends on ax-13 2379. See cbvaldw 2347 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2379. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvexd 2418* | Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2462. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker cbvexdw 2348 if possible. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbvaldva 2419* | Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker cbvaldvaw 2045 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvexdva 2420* | Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker cbvexdvaw 2046 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbval2 2421* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker cbval2v 2352 if possible. (Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-Sep-2023.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbval2OLD 2422* | Obsolete version of cbval2 2421 as of 11-Sep-2023. (Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2 2423* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker cbvex2v 2354 if possible. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 16-Jun-2019.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | cbval2vv 2424* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker cbval2vw 2047 if possible. (Contributed by NM, 4-Feb-2005.) Remove dependency on ax-10 2142. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2vv 2425* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker cbvex2vw 2048 if possible. (Contributed by NM, 26-Jul-1995.) Remove dependency on ax-10 2142. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | cbvex4v 2426* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker cbvex4vw 2049 if possible. (Contributed by NM, 26-Jul-1995.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒) | ||
Theorem | equs4 2427 | Lemma used in proofs of implicit substitution properties. The converse requires either a disjoint variable condition (sb56 2274) or a non-freeness hypothesis (equs45f 2471). Usage of this theorem is discouraged because it depends on ax-13 2379. See equs4v 2006 for a weaker version requiring fewer axioms. (Contributed by NM, 10-May-1993.) (Proof shortened by Mario Carneiro, 20-May-2014.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) (New usage is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | equsal 2428 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. See equsalvw 2010 and equsalv 2265 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsex 2429. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsex 2429 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. See equsexvw 2011 and equsexv 2266 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2428. See equsexALT 2430 for an alternate proof. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Feb-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | equsexALT 2430 | Alternate proof of equsex 2429. This proves the result directly, instead of as a corollary of equsal 2428 via equs4 2427. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2379 is ax6e 2390. This proof mimics that of equsal 2428 (in particular, note that pm5.32i 578, exbii 1849, 19.41 2235, mpbiran 708 correspond respectively to pm5.74i 274, albii 1821, 19.23 2209, a1bi 366). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | equsalh 2431 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. See equsalhw 2295 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexh 2432 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. See equsexhv 2296 for a version with a disjoint variable condition which does not require ax-13 2379. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | axc15 2433 |
Derivation of set.mm's original ax-c15 36185 from ax-c11n 36184 and the shorter
ax-12 2175 that has replaced it.
Theorem ax12 2434 shows the reverse derivation of ax-12 2175 from ax-c15 36185. Normally, axc15 2433 should be used rather than ax-c15 36185, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 26-Mar-2023.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | ax12 2434 | Rederivation of axiom ax-12 2175 from ax12v 2176 (used only via sp 2180) , axc11r 2375, and axc15 2433 (on top of Tarski's FOL). Since this version depends on ax-13 2379, usage of the weaker ax12v 2176, ax12w 2134, ax12i 1969 are preferred. (Contributed by NM, 22-Jan-2007.) Proof uses contemporary axioms. (Revised by Wolf Lammen, 8-Aug-2020.) (Proof shortened by BJ, 4-Jul-2021.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | ax12b 2435 | A bidirectional version of axc15 2433. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | ax13ALT 2436 | Alternate proof of ax13 2382 from FOL, sp 2180, and axc9 2389. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | axc11n 2437 | Derive set.mm's original ax-c11n 36184 from others. Commutation law for identical variable specifiers. The antecedent and consequent are true when 𝑥 and 𝑦 are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). If a disjoint variable condition is added on 𝑥 and 𝑦, then this becomes an instance of aevlem 2060. Use aecom 2438 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 10-May-1993.) (Revised by NM, 7-Nov-2015.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) (Revised by Wolf Lammen, 30-Nov-2019.) (Proof shortened by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 2-Jul-2021.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | aecom 2438 | Commutation law for identical variable specifiers. Both sides of the biconditional are true when 𝑥 and 𝑦 are substituted with the same variable. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 10-May-1993.) Change to a biconditional. (Revised by BJ, 26-Sep-2019.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 𝑦 = 𝑥) | ||
Theorem | aecoms 2439 | A commutation rule for identical variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | naecoms 2440 | A commutation rule for distinct variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | axc11 2441 | Show that ax-c11 36183 can be derived from ax-c11n 36184 in the form of axc11n 2437. Normally, axc11 2441 should be used rather than ax-c11 36183, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker axc11v 2262 when possible. (Contributed by NM, 16-May-2008.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | hbae 2442 | All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker hbaev 2064 when possible. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | hbnae 2443 | All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker hbnaev 2067 when possible. (Contributed by NM, 13-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | nfae 2444 | All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 | ||
Theorem | nfnae 2445 | All variables are effectively bound in a distinct variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker nfnaew 2150 when possible. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | hbnaes 2446 | Rule that applies hbnae 2443 to antecedent. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 15-May-1993.) (New usage is discouraged.) |
⊢ (∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) | ||
Theorem | axc16i 2447* | Inference with axc16 2259 as its conclusion. Usage of axc16 2259 is preferred since it requires fewer axioms. (Contributed by NM, 20-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16nfALT 2448* | Alternate proof of axc16nf 2261, shorter but requiring ax-11 2158 and ax-13 2379. (Contributed by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) | ||
Theorem | dral2 2449 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2379. Usage of albidv 1921 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) Allow a shortening of dral1 2450. (Revised by Wolf Lammen, 4-Mar-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓)) | ||
Theorem | dral1 2450 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker dral1v 2376 if possible. (Contributed by NM, 24-Nov-1994.) Remove dependency on ax-11 2158. (Revised by Wolf Lammen, 6-Sep-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | dral1ALT 2451 | Alternate proof of dral1 2450, shorter but requiring ax-11 2158. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | drex1 2452 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker drex1v 2377 if possible. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓)) | ||
Theorem | drex2 2453 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2379. Usage of exbidv 1922 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑧𝜑 ↔ ∃𝑧𝜓)) | ||
Theorem | drnf1 2454 | Formula-building lemma for use with the Distinctor Reduction Theorem. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker drnf1v 2378 if possible. (Contributed by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓)) | ||
Theorem | drnf2 2455 | Formula-building lemma for use with the Distinctor Reduction Theorem. Usage of this theorem is discouraged because it depends on ax-13 2379. Usage of nfbidv 1923 is preferred, which requires fewer axioms. (Contributed by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 5-May-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓)) | ||
Theorem | nfald2 2456 | Variation on nfald 2336 which adds the hypothesis that 𝑥 and 𝑦 are distinct in the inner subproof. Usage of this theorem is discouraged because it depends on ax-13 2379. Check out nfald 2336 for a version requiring fewer axioms. (Contributed by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) | ||
Theorem | nfexd2 2457 | Variation on nfexd 2337 which adds the hypothesis that 𝑥 and 𝑦 are distinct in the inner subproof. Usage of this theorem is discouraged because it depends on ax-13 2379. Check out nfexd 2337 for a version requiring fewer axioms. (Contributed by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) | ||
Theorem | exdistrf 2458 | Distribution of existential quantifiers, with a bound-variable hypothesis saying that 𝑦 is not free in 𝜑, but 𝑥 can be free in 𝜑 (and there is no distinct variable condition on 𝑥 and 𝑦). Usage of this theorem is discouraged because it depends on ax-13 2379. Check out exdistr 1955 for a version requiring fewer axioms. (Contributed by Mario Carneiro, 20-Mar-2013.) (Proof shortened by Wolf Lammen, 14-May-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑) ⇒ ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | dvelimf 2459 | Version of dvelimv 2463 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 1-Oct-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑧𝜓 & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓) | ||
Theorem | dvelimdf 2460 | Deduction form of dvelimf 2459. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑧𝜒) & ⊢ (𝜑 → (𝑧 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜒)) | ||
Theorem | dvelimh 2461 | Version of dvelim 2462 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2379. Check out dvelimhw 2355 for a version requiring fewer axioms. (Contributed by NM, 1-Oct-2002.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑧𝜓) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dvelim 2462* |
This theorem can be used to eliminate a distinct variable restriction on
𝑥 and 𝑧 and replace it with the
"distinctor" ¬ ∀𝑥𝑥 = 𝑦
as an antecedent. 𝜑 normally has 𝑧 free and can be read
𝜑(𝑧), and 𝜓 substitutes 𝑦 for
𝑧
and can be read
𝜑(𝑦). We do not require that 𝑥 and
𝑦
be distinct: if
they are not, the distinctor will become false (in multiple-element
domains of discourse) and "protect" the consequent.
To obtain a closed-theorem form of this inference, prefix the hypotheses with ∀𝑥∀𝑧, conjoin them, and apply dvelimdf 2460. Other variants of this theorem are dvelimh 2461 (with no distinct variable restrictions) and dvelimhw 2355 (that avoids ax-13 2379). Usage of this theorem is discouraged because it depends on ax-13 2379. Check out dvelimhw 2355 for a version requiring fewer axioms. (Contributed by NM, 23-Nov-1994.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dvelimv 2463* | Similar to dvelim 2462 with first hypothesis replaced by a distinct variable condition. Usage of this theorem is discouraged because it depends on ax-13 2379. Check out dvelimhw 2355 for a version requiring fewer axioms. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) (New usage is discouraged.) |
⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dvelimnf 2464* | Version of dvelim 2462 using "not free" notation. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓) | ||
Theorem | dveeq2ALT 2465* | Alternate proof of dveeq2 2385, shorter but requiring ax-11 2158. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | equvini 2466 | A variable introduction law for equality. Lemma 15 of [Monk2] p. 109, however we do not require 𝑧 to be distinct from 𝑥 and 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2379. See equvinv 2036 for a shorter proof requiring fewer axioms when 𝑧 is required to be distinct from 𝑥 and 𝑦. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 16-Sep-2023.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑧 = 𝑦)) | ||
Theorem | equviniOLD 2467 | Obsolete version of equvini 2466 as of 16-Sep-2023. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 15-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑧 = 𝑦)) | ||
Theorem | equvel 2468 | A variable elimination law for equality with no distinct variable requirements. Compare equvini 2466. Usage of this theorem is discouraged because it depends on ax-13 2379. Use equvelv 2038 when possible. (Contributed by NM, 1-Mar-2013.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.) |
⊢ (∀𝑧(𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → 𝑥 = 𝑦) | ||
Theorem | equs5a 2469 | A property related to substitution that unlike equs5 2472 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2379. This proof uses ax12 2434, see equs5aALT 2373 for an alternative one using ax-12 2175 but not ax13 2382. Usage of the weaker equs5av 2276 is preferred, which uses ax12v2 2177, but not ax-13 2379. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5e 2470 | A property related to substitution that unlike equs5 2472 does not require a distinctor antecedent. This proof uses ax12 2434, see equs5eALT 2374 for an alternative one using ax-12 2175 but not ax13 2382. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑)) | ||
Theorem | equs45f 2471 | Two ways of expressing substitution when 𝑦 is not free in 𝜑. The implication "to the left" is equs4 2427 and does not require the non-freeness hypothesis. Theorem sb56 2274 replaces the non-freeness hypothesis with a disjoint variable condition and equs5 2472 replaces it with a distinctor as antecedent. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 25-Apr-2008.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5 2472 | Lemma used in proofs of substitution properties. If there is a disjoint variable condition on 𝑥, 𝑦, then sb56 2274 can be used instead; if 𝑦 is not free in 𝜑, then equs45f 2471 can be used. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 14-May-1993.) (Revised by BJ, 1-Oct-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | dveel1 2473* | Quantifier introduction when one pair of variables is distinct. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → ∀𝑥 𝑦 ∈ 𝑧)) | ||
Theorem | dveel2 2474* | Quantifier introduction when one pair of variables is distinct. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)) | ||
Theorem | axc14 2475 |
Axiom ax-c14 36187 is redundant if we assume ax-5 1911.
Remark 9.6 in
[Megill] p. 448 (p. 16 of the preprint),
regarding axiom scheme C14'.
Note that 𝑤 is a dummy variable introduced in the proof. Its purpose is to satisfy the distinct variable requirements of dveel2 2474 and ax-5 1911. By the end of the proof it has vanished, and the final theorem has no distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 29-Jun-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦))) | ||
Theorem | sb6x 2476 | Equivalence involving substitution for a variable not free. Usage of this theorem is discouraged because it depends on ax-13 2379. Usage of sb6 2090 is preferred, which requires fewer axioms. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sbequ5 2477 | Substitution does not change an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 15-May-1993.) (New usage is discouraged.) |
⊢ ([𝑤 / 𝑧]∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | sbequ6 2478 | Substitution does not change a distinctor. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ ([𝑤 / 𝑧] ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | sb5rf 2479 | Reversed substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 20-Sep-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb6rf 2480 | Reversed substitution. For a version requiring disjoint variables, but fewer axioms, see sb6rfv 2365. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker sb6rfv 2365 if possible. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | ax12vALT 2481* | Alternate proof of ax12v2 2177, shorter, but depending on more axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | 2ax6elem 2482 | We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. This theorem merges two ax6e 2390 instances ∃𝑧𝑧 = 𝑥 and ∃𝑤𝑤 = 𝑦 into a common expression. Alan Sare contributed a variant of this theorem with distinct variable conditions before, see ax6e2nd 41264. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by Wolf Lammen, 27-Sep-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑤 𝑤 = 𝑧 → ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) | ||
Theorem | 2ax6e 2483* | We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. Version of 2ax6elem 2482 with a distinct variable constraint. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by Wolf Lammen, 28-Sep-2018.) (Proof shortened by Wolf Lammen, 3-Oct-2023.) (New usage is discouraged.) |
⊢ ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) | ||
Theorem | 2ax6eOLD 2484* | Obsolete version of 2ax6e 2483 as of 3-Oct-2023. (Contributed by Wolf Lammen, 28-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) | ||
Theorem | 2sb5rf 2485* | Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) Remove distinct variable constraints. (Revised by Wolf Lammen, 28-Sep-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 ⇒ ⊢ (𝜑 ↔ ∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)) | ||
Theorem | 2sb6rf 2486* | Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) Remove variable constraints. (Revised by Wolf Lammen, 28-Sep-2018.) (Proof shortened by Wolf Lammen, 13-Apr-2023.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 ⇒ ⊢ (𝜑 ↔ ∀𝑧∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)) | ||
Theorem | sbel2x 2487* | Elimination of double substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ [𝑦 / 𝑤][𝑥 / 𝑧]𝜑)) | ||
Theorem | sb4b 2488 | Simplified definition of substitution when variables are distinct. Version of sb6 2090 with a distinctor. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 27-May-1997.) Revise df-sb 2070. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))) | ||
Theorem | sb4bOLD 2489 | Obsolete version of sb4b 2488 as of 21-Feb-2024. (Contributed by NM, 27-May-1997.) Revise df-sb 2070. (Revised by Wolf Lammen, 25-Jul-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))) | ||
Theorem | sb3b 2490 | Simplified definition of substitution when variables are distinct. This is the biconditional strengthening of sb3 2491. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by BJ, 6-Oct-2018.) Shorten sb3 2491. (Revised by Wolf Lammen, 21-Feb-2021.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | sb3 2491 | One direction of a simplified definition of substitution when variables are distinct. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb1 2492 | One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb5 2273) or a non-freeness hypothesis (sb5f 2516). Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker sb1v 2092 when possible. (Contributed by NM, 13-May-1993.) Revise df-sb 2070. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb2 2493 | One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb6 2090) or a non-freeness hypothesis (sb6f 2515). Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 13-May-1993.) Revise df-sb 2070. (Revised by Wolf Lammen, 26-Jul-2023.) (New usage is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑) | ||
Theorem | sb3OLD 2494 | Obsolete version of sb3 2491 as of 21-Feb-2024. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb4OLD 2495 | Obsolete as of 30-Jul-2023. Use sb4b 2488 instead. One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 14-May-1993.) Revise df-sb 2070. (Revised by Wolf Lammen, 25-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sb1OLD 2496 | Obsolete version of sb1 2492 as of 21-Feb-2024. (Contributed by NM, 13-May-1993.) Revise df-sb 2070. (Revised by Wolf Lammen, 29-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb3bOLD 2497 | Obsolete version of sb3b 2490 as of 21-Feb-2024. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | sb4a 2498 | A version of one implication of sb4b 2488 that does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker sb4av 2242 when possible. (Contributed by NM, 2-Feb-2007.) Revise df-sb 2070. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.) |
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
Theorem | dfsb1 2499 | Alternate definition of substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). This was the original definition before df-sb 2070. Note that it does not require dummy variables in its definiens; this is done by having 𝑥 free in the first conjunct and bound in the second. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by BJ, 9-Jul-2023.) Revise df-sb 2070. (Revised by Wolf Lammen, 29-Jul-2023.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | hbsb2 2500 | Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |