![]() |
Metamath
Proof Explorer Theorem List (p. 37 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | spc2d 3601* | Specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.) |
⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑦𝜒 & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∀𝑥∀𝑦𝜓 → 𝜒)) | ||
Theorem | spc3egv 3602* | Existential specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.) Avoid ax-10 2138 and ax-11 2154. (Revised by GG, 20-Aug-2023.) (Proof shortened by Wolf Lammen, 25-Aug-2023.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → ∃𝑥∃𝑦∃𝑧𝜑)) | ||
Theorem | spc3gv 3603* | Specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥∀𝑦∀𝑧𝜑 → 𝜓)) | ||
Theorem | spcv 3604* | Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spcev 3605* | Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜓 → ∃𝑥𝜑) | ||
Theorem | spc2ev 3606* | Existential specialization, using implicit substitution. (Contributed by NM, 3-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜓 → ∃𝑥∃𝑦𝜑) | ||
Theorem | rspct 3607* | A closed version of rspc 3609. (Contributed by Andrew Salmon, 6-Jun-2011.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))) | ||
Theorem | rspcdf 3608* | Restricted specialization, using implicit substitution. (Contributed by Emmett Weisz, 16-Jan-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) | ||
Theorem | rspc 3609* | Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) | ||
Theorem | rspce 3610* | Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro, 11-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | rspcimdv 3611* | Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) | ||
Theorem | rspcimedv 3612* | Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rspcdv 3613* | Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) | ||
Theorem | rspcedv 3614* | Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rspcebdv 3615* | Restricted existential specialization, using implicit substitution in both directions. (Contributed by AV, 8-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑥 = 𝐴) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ 𝜒)) | ||
Theorem | rspcdv2 3616* | Restricted specialization, using implicit substitution. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | rspcv 3617* | Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2138, ax-11 2154, ax-12 2174. (Revised by SN, 12-Dec-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) | ||
Theorem | rspccv 3618* | Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) | ||
Theorem | rspcva 3619* | Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓) | ||
Theorem | rspccva 3620* | Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓) | ||
Theorem | rspcev 3621* | Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2138, ax-11 2154, ax-12 2174. (Revised by SN, 12-Dec-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | rspcdva 3622* | Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | rspcedvd 3623* | Restricted existential specialization, using implicit substitution. Variant of rspcedv 3614. (Contributed by AV, 27-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) | ||
Theorem | rspcedvdw 3624* | Version of rspcedvd 3623 where the implicit substitution hypothesis does not have an antecedent, which also avoids a disjoint variable condition on 𝜑, 𝑥. (Contributed by SN, 20-Aug-2024.) |
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) | ||
Theorem | rspceb2dv 3625* | Restricted existential specialization, using implicit substitution in both directions. (Contributed by Zhi Wang, 28-Sep-2024.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜓 → 𝜒)) & ⊢ ((𝜑 ∧ 𝜒) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ 𝜒)) | ||
Theorem | rspcime 3626* | Prove a restricted existential. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) | ||
Theorem | rspceaimv 3627* | Restricted existential specialization of a universally quantified implication. (Contributed by BJ, 24-Aug-2022.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒)) | ||
Theorem | rspcedeq1vd 3628* | Restricted existential specialization, using implicit substitution. Variant of rspcedvd 3623 for equations, in which the left hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷) | ||
Theorem | rspcedeq2vd 3629* | Restricted existential specialization, using implicit substitution. Variant of rspcedvd 3623 for equations, in which the right hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷) | ||
Theorem | rspc2 3630* | Restricted specialization with two quantifiers, using implicit substitution. (Contributed by NM, 9-Nov-2012.) |
⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) | ||
Theorem | rspc2gv 3631* | Restricted specialization with two quantifiers, using implicit substitution. (Contributed by BJ, 2-Dec-2021.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 𝜑 → 𝜓)) | ||
Theorem | rspc2v 3632* | 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) | ||
Theorem | rspc2va 3633* | 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓) | ||
Theorem | rspc2ev 3634* | 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑) | ||
Theorem | 2rspcedvdw 3635* | Double application of rspcedvdw 3624. (Contributed by SN, 24-Aug-2024.) |
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝜓) | ||
Theorem | rspc2dv 3636* | 2-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 6-Mar-2025.) |
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝑦 = 𝐵 → (𝜃 ↔ 𝜒)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜓) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | rspc3v 3637* | 3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓)) | ||
Theorem | rspc3ev 3638* | 3-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑) | ||
Theorem | 3rspcedvdw 3639* | Triple application of rspcedvdw 3624. (Contributed by SN, 20-Aug-2024.) |
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜏)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) & ⊢ (𝜑 → 𝜏) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∃𝑧 ∈ 𝑍 𝜓) | ||
Theorem | rspc3dv 3640* | 3-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2025.) |
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝑦 = 𝐵 → (𝜃 ↔ 𝜏)) & ⊢ (𝑧 = 𝐶 → (𝜏 ↔ 𝜒)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 𝜓) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐸) & ⊢ (𝜑 → 𝐶 ∈ 𝐹) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | rspc4v 3641* | 4-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 7-Feb-2025.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜏)) & ⊢ (𝑤 = 𝐷 → (𝜏 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈)) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 𝜑 → 𝜓)) | ||
Theorem | rspc6v 3642* | 6-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 20-Feb-2025.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜏)) & ⊢ (𝑤 = 𝐷 → (𝜏 ↔ 𝜂)) & ⊢ (𝑝 = 𝐸 → (𝜂 ↔ 𝜁)) & ⊢ (𝑞 = 𝐹 → (𝜁 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈) ∧ (𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊)) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 𝜑 → 𝜓)) | ||
Theorem | rspc8v 3643* | 8-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 20-Feb-2025.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜏)) & ⊢ (𝑤 = 𝐷 → (𝜏 ↔ 𝜂)) & ⊢ (𝑝 = 𝐸 → (𝜂 ↔ 𝜁)) & ⊢ (𝑞 = 𝐹 → (𝜁 ↔ 𝜎)) & ⊢ (𝑟 = 𝐺 → (𝜎 ↔ 𝜌)) & ⊢ (𝑠 = 𝐻 → (𝜌 ↔ 𝜓)) ⇒ ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈)) ∧ ((𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) ∧ (𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌))) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜑 → 𝜓)) | ||
Theorem | rspceeqv 3644* | Restricted existential specialization in an equality, using implicit substitution. (Contributed by BJ, 2-Sep-2022.) |
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐸 = 𝐷) → ∃𝑥 ∈ 𝐵 𝐸 = 𝐶) | ||
Theorem | ralxpxfr2d 3645* | Transfer a universal quantifier between one variable with pair-like semantics and two. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝑥 = 𝐴)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐷 𝜒)) | ||
Theorem | rexraleqim 3646* | Statement following from existence and generalization with equality. (Contributed by AV, 9-Feb-2019.) |
⊢ (𝑥 = 𝑧 → (𝜓 ↔ 𝜑)) & ⊢ (𝑧 = 𝑌 → (𝜑 ↔ 𝜃)) ⇒ ⊢ ((∃𝑧 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 = 𝑌)) → 𝜃) | ||
Theorem | eqvincg 3647* | A variable introduction law for class equality, closed form. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵))) | ||
Theorem | eqvinc 3648* | 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 3649 | 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 3650* | Two ways to express substitution of 𝐴 for 𝑥 in 𝜑. This is the analogue for classes of sbalex 2239. (Contributed by NM, 2-Mar-1995.) (Revised by BJ, 27-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) | ||
Theorem | ceqex 3651* | Equality implies equivalence with substitution. (Contributed by NM, 2-Mar-1995.) (Proof shortened by BJ, 1-May-2019.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) | ||
Theorem | ceqsexg 3652* | 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 3653* | Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 29-Dec-1996.) Drop ax-10 2138 and ax-12 2174. (Revised by GG, 1-Dec-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsrexv 3654* | Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsrexbv 3655* | Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by Mario Carneiro, 14-Mar-2014.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) | ||
Theorem | ceqsralbv 3656* | Elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)) | ||
Theorem | ceqsrex2v 3657* | Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 29-Oct-2005.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝜑) ↔ 𝜒)) | ||
Theorem | clel2g 3658* | 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 2174. (Revised by BJ, 1-Sep-2024.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))) | ||
Theorem | clel2 3659* | Alternate definition of membership when the member is a set. (Contributed by NM, 18-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | clel3g 3660* | Alternate definition of membership in a set. (Contributed by NM, 13-Aug-2005.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥))) | ||
Theorem | clel3 3661* | Alternate definition of membership in a set. (Contributed by NM, 18-Aug-1993.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥)) | ||
Theorem | clel4g 3662* | Alternate definition of membership in a set. (Contributed by NM, 18-Aug-1993.) Strengthen from sethood hypothesis to sethood antecedent and avoid ax-12 2174. (Revised by BJ, 1-Sep-2024.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐵 → 𝐴 ∈ 𝑥))) | ||
Theorem | clel4 3663* | Alternate definition of membership in a set. (Contributed by NM, 18-Aug-1993.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐵 → 𝐴 ∈ 𝑥)) | ||
Theorem | clel5 3664* | 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 2138, ax-11 2154, and ax-12 2174. (Revised by Steven Nguyen, 19-May-2023.) |
⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑋 = 𝑥) | ||
Theorem | pm13.183 3665* | 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 2374. (Revised by Wolf Lammen, 29-Apr-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 ↔ ∀𝑧(𝑧 = 𝐴 ↔ 𝑧 = 𝐵))) | ||
Theorem | rr19.3v 3666* | Restricted quantifier version of Theorem 19.3 of [Margaris] p. 89. We don't need the nonempty class condition of r19.3rzv 4504 when there is an outer quantifier. (Contributed by NM, 25-Oct-2012.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rr19.28v 3667* | Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. We don't need the nonempty class condition of r19.28zv 4506 when there is an outer quantifier. (Contributed by NM, 29-Oct-2012.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | elab6g 3668* | Membership in a class abstraction. Class version of sb6 2082. (Contributed by SN, 5-Oct-2024.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))) | ||
Theorem | elabd2 3669* | Membership in a class abstraction, using implicit substitution. Deduction version of elab 3680. (Contributed by GG, 12-Oct-2024.) (Revised by BJ, 16-Oct-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = {𝑥 ∣ 𝜓}) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝜒)) | ||
Theorem | elabd3 3670* | Membership in a class abstraction, using implicit substitution. Deduction version of elab 3680. (Contributed by GG, 12-Oct-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜒)) | ||
Theorem | elabgt 3671* | Membership in a class abstraction, using implicit substitution. (Closed theorem version of elabg 3676.) (Contributed by NM, 7-Nov-2005.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom usage. (Revised by GG, 12-Oct-2024.) (Proof shortend by Wolf Lammen, 11-May-2025.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elabgtOLD 3672* | Obsolete version of elabgt 3671 as of 11-May-2025. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom usage. (Revised by GG, 12-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elabgtOLDOLD 3673* | Obsolete version of elabgt 3671 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 3674 | 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 3675* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) | ||
Theorem | elabg 3676* | 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 2374. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2138, ax-11 2154, ax-12 2174. (Revised by SN, 5-Oct-2024.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elabgOLD 3677* | Obsolete version of elabg 3676 as of 5-Oct-2024. (Contributed by NM, 14-Apr-1995.) Remove dependency on ax-13 2374. (Revised by SN, 23-Nov-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elabgw 3678* | Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on 𝑥 and 𝐴. This is to elabg 3676 what sbievw2 2095 is to sbievw 2090. (Contributed by SN, 20-Apr-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒)) | ||
Theorem | elab2gw 3679* | Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on 𝑥 and 𝐴, which is not usually significant since 𝐵 is usually a constant. (Contributed by SN, 16-May-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜒)) | ||
Theorem | elab 3680* | 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 2138, ax-11 2154, ax-12 2174. (Revised by SN, 5-Oct-2024.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) | ||
Theorem | elabOLD 3681* | Obsolete version of elab 3680 as of 5-Oct-2024. (Contributed by NM, 1-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) | ||
Theorem | elab2g 3682* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓)) | ||
Theorem | elabd 3683* | Explicit demonstration the class {𝑥 ∣ 𝜓} is not empty by the example 𝐴. (Contributed by RP, 12-Aug-2020.) (Revised by AV, 23-Mar-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝜒) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∣ 𝜓}) | ||
Theorem | elab2 3684* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓) | ||
Theorem | elab4g 3685* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 17-Oct-2012.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ V ∧ 𝜓)) | ||
Theorem | elab3gf 3686 | Membership in a class abstraction, with a weaker antecedent than elabgf 3674. (Contributed by NM, 6-Sep-2011.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝜓 → 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elab3g 3687* | Membership in a class abstraction, with a weaker antecedent than elabg 3676. (Contributed by NM, 29-Aug-2006.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝜓 → 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elab3 3688* | Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.) (Revised by AV, 16-Aug-2024.) |
⊢ (𝜓 → 𝐴 ∈ 𝑉) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) | ||
Theorem | elrabi 3689* | 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 2138, ax-11 2154, ax-12 2174. (Revised by SN, 5-Aug-2024.) |
⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉) | ||
Theorem | elrabf 3690 | 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 3691 | Abstract builder using the constant wff ⊤. (Contributed by Thierry Arnoux, 4-May-2020.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
Theorem | rabeqcOLD 3692* | Obsolete version of rabeqc 3445 as of 15-Jan-2025. (Contributed by AV, 20-Apr-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = 𝐴 | ||
Theorem | elrab3t 3693* | Membership in a restricted class abstraction, using implicit substitution. (Closed theorem version of elrab3 3695.) (Contributed by Thierry Arnoux, 31-Aug-2017.) |
⊢ ((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elrab 3694* | Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.) Remove dependency on ax-13 2374. (Revised by Steven Nguyen, 23-Nov-2022.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) | ||
Theorem | elrab3 3695* | Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | elrabd 3696* | Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 3694. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | elrab2 3697* | Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝐶 = {𝑥 ∈ 𝐵 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) | ||
Theorem | elrab2w 3698* | Membership in a restricted class abstraction. This is to elrab2 3697 what elab2gw 3679 is to elab2g 3682. (Contributed by SN, 2-Sep-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ 𝐶 = {𝑥 ∈ 𝐵 ∣ 𝜑} ⇒ ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜒)) | ||
Theorem | ralab 3699* | Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) Reduce axiom usage. (Revised by GG, 2-Nov-2024.) |
⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝜓 → 𝜒)) | ||
Theorem | ralabOLD 3700* | Obsolete version of ralab 3699 as of 2-Nov-2024. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∀𝑥(𝜓 → 𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |