Home | Metamath
Proof Explorer Theorem List (p. 36 of 461) | < 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: | Metamath Proof Explorer
(1-28865) |
Hilbert Space Explorer
(28866-30388) |
Users' Mathboxes
(30389-46009) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | spcdv 3501* | Rule of specialization, using implicit substitution. Analogous to rspcdv 3521. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
Theorem | spcimedv 3502* | Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥𝜓)) | ||
Theorem | spcgv 3503* | Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.) Avoid ax-10 2145, ax-11 2162. (Revised by Wolf Lammen, 25-Aug-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | spcegv 3504* | Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2145, ax-11 2162. (Revised by Wolf Lammen, 25-Aug-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) | ||
Theorem | spcedv 3505* | Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12-Aug-2020.) (Revised by AV, 16-Aug-2024.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝜒) & ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | spc2egv 3506* | Existential specialization with two quantifiers, using implicit substitution. (Contributed by NM, 3-Aug-1995.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝜓 → ∃𝑥∃𝑦𝜑)) | ||
Theorem | spc2gv 3507* | Specialization with two quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥∀𝑦𝜑 → 𝜓)) | ||
Theorem | spc2ed 3508* | Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.) |
⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑦𝜒 & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (𝜒 → ∃𝑥∃𝑦𝜓)) | ||
Theorem | spc2d 3509* | Specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.) |
⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑦𝜒 & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∀𝑥∀𝑦𝜓 → 𝜒)) | ||
Theorem | spc3egv 3510* | Existential specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.) Avoid ax-10 2145 and ax-11 2162. (Revised by Gino Giotto, 20-Aug-2023.) (Proof shortened by Wolf Lammen, 25-Aug-2023.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → ∃𝑥∃𝑦∃𝑧𝜑)) | ||
Theorem | spc3gv 3511* | Specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥∀𝑦∀𝑧𝜑 → 𝜓)) | ||
Theorem | spcv 3512* | Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spcev 3513* | Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜓 → ∃𝑥𝜑) | ||
Theorem | spc2ev 3514* | Existential specialization, using implicit substitution. (Contributed by NM, 3-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜓 → ∃𝑥∃𝑦𝜑) | ||
Theorem | rspct 3515* | A closed version of rspc 3517. (Contributed by Andrew Salmon, 6-Jun-2011.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))) | ||
Theorem | rspcdf 3516* | Restricted specialization, using implicit substitution. (Contributed by Emmett Weisz, 16-Jan-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) | ||
Theorem | rspc 3517* | Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) | ||
Theorem | rspce 3518* | Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro, 11-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | rspcimdv 3519* | Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) | ||
Theorem | rspcimedv 3520* | Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rspcdv 3521* | Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) | ||
Theorem | rspcedv 3522* | Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rspcebdv 3523* | Restricted existential specialization, using implicit substitution in both directions. (Contributed by AV, 8-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑥 = 𝐴) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ 𝜒)) | ||
Theorem | rspcv 3524* | Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2145, ax-11 2162, ax-12 2179. (Revised by SN, 12-Dec-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) | ||
Theorem | rspcvOLD 3525* | Obsolete version of rspcv 3524 as of 12-Dec-2023. Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) | ||
Theorem | rspccv 3526* | Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) | ||
Theorem | rspcva 3527* | Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓) | ||
Theorem | rspccva 3528* | Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓) | ||
Theorem | rspcev 3529* | Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2145, ax-11 2162, ax-12 2179. (Revised by SN, 12-Dec-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | rspcevOLD 3530* | Obsolete version of rspce 3518 as of 12-Dec-2023. Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | rspcdva 3531* | Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | rspcedvd 3532* | Restricted existential specialization, using implicit substitution. Variant of rspcedv 3522. (Contributed by AV, 27-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) | ||
Theorem | rspcime 3533* | Prove a restricted existential. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) | ||
Theorem | rspceaimv 3534* | Restricted existential specialization of a universally quantified implication. (Contributed by BJ, 24-Aug-2022.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒)) | ||
Theorem | rspcedeq1vd 3535* | Restricted existential specialization, using implicit substitution. Variant of rspcedvd 3532 for equations, in which the left hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷) | ||
Theorem | rspcedeq2vd 3536* | Restricted existential specialization, using implicit substitution. Variant of rspcedvd 3532 for equations, in which the right hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷) | ||
Theorem | rspc2 3537* | Restricted specialization with two quantifiers, using implicit substitution. (Contributed by NM, 9-Nov-2012.) |
⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) | ||
Theorem | rspc2gv 3538* | Restricted specialization with two quantifiers, using implicit substitution. (Contributed by BJ, 2-Dec-2021.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 𝜑 → 𝜓)) | ||
Theorem | rspc2v 3539* | 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) | ||
Theorem | rspc2va 3540* | 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓) | ||
Theorem | rspc2ev 3541* | 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑) | ||
Theorem | rspc3v 3542* | 3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓)) | ||
Theorem | rspc3ev 3543* | 3-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑) | ||
Theorem | rspceeqv 3544* | Restricted existential specialization in an equality, using implicit substitution. (Contributed by BJ, 2-Sep-2022.) |
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐸 = 𝐷) → ∃𝑥 ∈ 𝐵 𝐸 = 𝐶) | ||
Theorem | ralxpxfr2d 3545* | Transfer a universal quantifier between one variable with pair-like semantics and two. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝑥 = 𝐴)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐷 𝜒)) | ||
Theorem | rexraleqim 3546* | Statement following from existence and generalization with equality. (Contributed by AV, 9-Feb-2019.) |
⊢ (𝑥 = 𝑧 → (𝜓 ↔ 𝜑)) & ⊢ (𝑧 = 𝑌 → (𝜑 ↔ 𝜃)) ⇒ ⊢ ((∃𝑧 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 = 𝑌)) → 𝜃) | ||
Theorem | eqvincg 3547* | A variable introduction law for class equality, closed form. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵))) | ||
Theorem | eqvinc 3548* | A variable introduction law for class equality. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Proof shortened by Thierry Arnoux, 23-Jan-2022.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵)) | ||
Theorem | eqvincf 3549 | A variable introduction law for class equality, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Sep-2003.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵)) | ||
Theorem | alexeqg 3550* | Two ways to express substitution of 𝐴 for 𝑥 in 𝜑. This is the analogue for classes of sbalex 2244. (Contributed by NM, 2-Mar-1995.) (Revised by BJ, 27-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) | ||
Theorem | ceqex 3551* | Equality implies equivalence with substitution. (Contributed by NM, 2-Mar-1995.) (Proof shortened by BJ, 1-May-2019.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) | ||
Theorem | ceqsexg 3552* | A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 11-Oct-2004.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsexgv 3553* | Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 29-Dec-1996.) Drop ax-10 2145 and ax-12 2179. (Revised by Gino Giotto, 1-Dec-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsexgvOLD 3554* | Obsolete version of ceqsexgv 3553 as of 1-Dec-2023. (Contributed by NM, 29-Dec-1996.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsrexv 3555* | Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsrexbv 3556* | Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by Mario Carneiro, 14-Mar-2014.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) | ||
Theorem | ceqsrex2v 3557* | Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 29-Oct-2005.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝜑) ↔ 𝜒)) | ||
Theorem | clel2g 3558* | Alternate definition of membership when the member is a set. (Contributed by NM, 18-Aug-1993.) Strengthen from sethood hypothesis to sethood antecedent. (Revised by BJ, 12-Feb-2022.) Avoid ax-12 2179. (Revised by BJ, 1-Sep-2024.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))) | ||
Theorem | clel2gOLD 3559* | Obsolete version of clel2g 3558 as of 1-Sep-2024. (Contributed by NM, 18-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))) | ||
Theorem | clel2 3560* | Alternate definition of membership when the member is a set. (Contributed by NM, 18-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | clel3g 3561* | Alternate definition of membership in a set. (Contributed by NM, 13-Aug-2005.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥))) | ||
Theorem | clel3 3562* | Alternate definition of membership in a set. (Contributed by NM, 18-Aug-1993.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥)) | ||
Theorem | clel4g 3563* | Alternate definition of membership in a set. (Contributed by NM, 18-Aug-1993.) Strengthen from sethood hypothesis to sethood antecedent and avoid ax-12 2179. (Revised by BJ, 1-Sep-2024.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐵 → 𝐴 ∈ 𝑥))) | ||
Theorem | clel4 3564* | Alternate definition of membership in a set. (Contributed by NM, 18-Aug-1993.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐵 → 𝐴 ∈ 𝑥)) | ||
Theorem | clel4OLD 3565* | Obsolete version of clel4 3564 as of 1-Sep-2024. (Contributed by NM, 18-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐵 → 𝐴 ∈ 𝑥)) | ||
Theorem | clel5 3566* | Alternate definition of class membership: a class 𝑋 is an element of another class 𝐴 iff there is an element of 𝐴 equal to 𝑋. (Contributed by AV, 13-Nov-2020.) Remove use of ax-10 2145, ax-11 2162, and ax-12 2179. (Revised by Steven Nguyen, 19-May-2023.) |
⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑋 = 𝑥) | ||
Theorem | pm13.183 3567* | Compare theorem *13.183 in [WhiteheadRussell] p. 178. Only 𝐴 is required to be a set. (Contributed by Andrew Salmon, 3-Jun-2011.) Avoid ax-13 2373. (Revised by Wolf Lammen, 29-Apr-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 ↔ ∀𝑧(𝑧 = 𝐴 ↔ 𝑧 = 𝐵))) | ||
Theorem | rr19.3v 3568* | Restricted quantifier version of Theorem 19.3 of [Margaris] p. 89. We don't need the nonempty class condition of r19.3rzv 4395 when there is an outer quantifier. (Contributed by NM, 25-Oct-2012.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rr19.28v 3569* | Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. We don't need the nonempty class condition of r19.28zv 4397 when there is an outer quantifier. (Contributed by NM, 29-Oct-2012.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | elab6g 3570* | Membership in a class abstraction. Class version of sb6 2095. (Contributed by SN, 5-Oct-2024.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))) | ||
Theorem | elabd2 3571* | Membership in a class abstraction, using implicit substitution. Deduction version of elab 3578. (Contributed by Gino Giotto, 12-Oct-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜒)) | ||
Theorem | elabgt 3572* | Membership in a class abstraction, using implicit substitution. (Closed theorem version of elabg 3576.) (Contributed by NM, 7-Nov-2005.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom usage. (Revised by Gino Giotto, 12-Oct-2024.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elabgtOLD 3573* | Obsolete version of elabgt 3572 as of 12-Oct-2024. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elabgf 3574 | Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) (Revised by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elabf 3575* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) | ||
Theorem | elabg 3576* | Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2373. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2145, ax-11 2162, ax-12 2179. (Revised by SN, 5-Oct-2024.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elabgOLD 3577* | Obsolete version of elabg 3576 as of 5-Oct-2024. (Contributed by NM, 14-Apr-1995.) Remove dependency on ax-13 2373. (Revised by SN, 23-Nov-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elab 3578* | Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 1-Aug-1994.) Avoid ax-10 2145, ax-11 2162, ax-12 2179. (Revised by SN, 5-Oct-2024.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) | ||
Theorem | elabOLD 3579* | Obsolete version of elab 3578 as of 5-Oct-2024. (Contributed by NM, 1-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) | ||
Theorem | elab2g 3580* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓)) | ||
Theorem | elabd 3581* | Explicit demonstration the class {𝑥 ∣ 𝜓} is not empty by the example 𝐴. (Contributed by RP, 12-Aug-2020.) (Revised by AV, 23-Mar-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝜒) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∣ 𝜓}) | ||
Theorem | elab2 3582* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓) | ||
Theorem | elab4g 3583* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 17-Oct-2012.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ V ∧ 𝜓)) | ||
Theorem | elab3gf 3584 | Membership in a class abstraction, with a weaker antecedent than elabgf 3574. (Contributed by NM, 6-Sep-2011.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝜓 → 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elab3g 3585* | Membership in a class abstraction, with a weaker antecedent than elabg 3576. (Contributed by NM, 29-Aug-2006.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝜓 → 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elab3 3586* | Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.) (Revised by AV, 16-Aug-2024.) |
⊢ (𝜓 → 𝐴 ∈ 𝑉) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) | ||
Theorem | elrabi 3587* | Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.) Remove disjoint variable condition on 𝐴, 𝑥 and avoid ax-10 2145, ax-11 2162, ax-12 2179. (Revised by SN, 5-Aug-2024.) |
⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉) | ||
Theorem | elrabiOLD 3588* | Obsolete version of elrabi 3587 as of 5-Aug-2024. (Contributed by Alexander van der Vekens, 31-Dec-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉) | ||
Theorem | elrabf 3589 | Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) | ||
Theorem | rabtru 3590 | Abstract builder using the constant wff ⊤. (Contributed by Thierry Arnoux, 4-May-2020.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
Theorem | rabeqc 3591* | A restricted class abstraction equals the restricting class if its condition follows from the membership of the free setvar variable in the restricting class. (Contributed by AV, 20-Apr-2022.) |
⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = 𝐴 | ||
Theorem | elrab3t 3592* | Membership in a restricted class abstraction, using implicit substitution. (Closed theorem version of elrab3 3594.) (Contributed by Thierry Arnoux, 31-Aug-2017.) |
⊢ ((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elrab 3593* | Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.) Remove dependency on ax-13 2373. (Revised by Steven Nguyen, 23-Nov-2022.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) | ||
Theorem | elrab3 3594* | Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elrabd 3595* | Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 3593. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | elrab2 3596* | Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐶 = {𝑥 ∈ 𝐵 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) | ||
Theorem | ralab 3597* | Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝜓 → 𝜒)) | ||
Theorem | ralrab 3598* | Universal quantification over a restricted class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) | ||
Theorem | rexab 3599* | Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 23-Jan-2014.) (Revised by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∃𝑥(𝜓 ∧ 𝜒)) | ||
Theorem | rexrab 3600* | Existential quantification over a class abstraction. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |