![]() |
Metamath
Proof Explorer Theorem List (p. 36 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 | elexd 3501 | If a class is a member of another class, then it is a set. Deduction associated with elex 3498. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ∈ V) | ||
Theorem | elex2OLD 3502* | Obsolete version of elex2 2815 as of 30-Nov-2024. (Contributed by Alan Sare, 25-Sep-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) | ||
Theorem | elex22 3503* | If two classes each contain another class, then both contain some set. (Contributed by Alan Sare, 24-Oct-2011.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | ||
Theorem | prcnel 3504 | A proper class doesn't belong to any class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof shortened by AV, 14-Nov-2020.) |
⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 ∈ 𝑉) | ||
Theorem | ralv 3505 | A universal quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.) |
⊢ (∀𝑥 ∈ V 𝜑 ↔ ∀𝑥𝜑) | ||
Theorem | rexv 3506 | An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.) |
⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑) | ||
Theorem | reuv 3507 | A unique existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 1-Nov-2010.) |
⊢ (∃!𝑥 ∈ V 𝜑 ↔ ∃!𝑥𝜑) | ||
Theorem | rmov 3508 | An at-most-one quantifier restricted to the universe is unrestricted. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
⊢ (∃*𝑥 ∈ V 𝜑 ↔ ∃*𝑥𝜑) | ||
Theorem | rabab 3509 | A class abstraction restricted to the universe is unrestricted. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ {𝑥 ∈ V ∣ 𝜑} = {𝑥 ∣ 𝜑} | ||
Theorem | rexcom4b 3510* | Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑) | ||
Theorem | ceqsal1t 3511 | One direction of ceqsalt 3512 is based on fewer assumptions and fewer axioms. It is at the same time the reverse direction of vtoclgft 3551. Extracted from a proof of ceqsalt 3512. (Contributed by Wolf Lammen, 25-Mar-2025.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝜓 → ∀𝑥(𝑥 = 𝐴 → 𝜑))) | ||
Theorem | ceqsalt 3512* | Closed theorem version of ceqsalg 3514. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsralt 3513* | Restricted quantifier version of ceqsalt 3512. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsalg 3514* | A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. For an alternate proof, see ceqsalgALT 3515. (Contributed by NM, 29-Oct-2003.) (Proof shortened by BJ, 29-Sep-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsalgALT 3515* | Alternate proof of ceqsalg 3514, not using ceqsalt 3512. (Contributed by NM, 29-Oct-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Revised by BJ, 29-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsal 3516* | A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.) Avoid df-clab 2712. (Revised by Wolf Lammen, 23-Jan-2025.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) | ||
Theorem | ceqsalALT 3517* | A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. Shorter proof uses df-clab 2712. (Contributed by NM, 18-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) | ||
Theorem | ceqsalv 3518* | A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.) Avoid ax-12 2174. (Revised by SN, 8-Sep-2024.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) | ||
Theorem | ceqsralv 3519* | Restricted quantifier version of ceqsalv 3518. (Contributed by NM, 21-Jun-2013.) Avoid ax-9 2115, ax-12 2174, ax-ext 2705. (Revised by SN, 8-Sep-2024.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | gencl 3520* | Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.) |
⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝐵)) & ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝜒 → 𝜑) ⇒ ⊢ (𝜃 → 𝜓) | ||
Theorem | 2gencl 3521* | Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.) |
⊢ (𝐶 ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑅 𝐴 = 𝐶) & ⊢ (𝐷 ∈ 𝑆 ↔ ∃𝑦 ∈ 𝑅 𝐵 = 𝐷) & ⊢ (𝐴 = 𝐶 → (𝜑 ↔ 𝜓)) & ⊢ (𝐵 = 𝐷 → (𝜓 ↔ 𝜒)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → 𝜑) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 𝜒) | ||
Theorem | 3gencl 3522* | Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.) |
⊢ (𝐷 ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑅 𝐴 = 𝐷) & ⊢ (𝐹 ∈ 𝑆 ↔ ∃𝑦 ∈ 𝑅 𝐵 = 𝐹) & ⊢ (𝐺 ∈ 𝑆 ↔ ∃𝑧 ∈ 𝑅 𝐶 = 𝐺) & ⊢ (𝐴 = 𝐷 → (𝜑 ↔ 𝜓)) & ⊢ (𝐵 = 𝐹 → (𝜓 ↔ 𝜒)) & ⊢ (𝐶 = 𝐺 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → 𝜑) ⇒ ⊢ ((𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆) → 𝜃) | ||
Theorem | cgsexg 3523* | Implicit substitution inference for general classes. (Contributed by NM, 26-Aug-2007.) |
⊢ (𝑥 = 𝐴 → 𝜒) & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝜒 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | cgsex2g 3524* | Implicit substitution inference for general classes. (Contributed by NM, 26-Jul-1995.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝜒) & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(𝜒 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | cgsex4g 3525* | An implicit substitution inference for 4 general classes. (Contributed by NM, 5-Aug-1995.) Avoid ax-10 2138, ax-11 2154. (Revised by GG, 28-Jun-2024.) Avoid ax-9 2115, ax-ext 2705. (Revised by Wolf Lammen, 21-Mar-2025.) |
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → 𝜒) & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | cgsex4gOLD 3526* | Obsolete version of cgsex4g 3525 as of 21-Mar-2025. (Contributed by NM, 5-Aug-1995.) Avoid ax-10 2138, ax-11 2154. (Revised by GG, 28-Jun-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → 𝜒) & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsex 3527* | Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) (Revised by Mario Carneiro, 10-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Jan-2025.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | ceqsexOLD 3528* | Obsolete version of ceqsex 3527 as of 22-Jan-2025. (Contributed by NM, 2-Mar-1995.) (Revised by Mario Carneiro, 10-Oct-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | ceqsexv 3529* | Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2174. (Revised by GG, 12-Oct-2024.) (Proof shortened by Wolf Lammen, 22-Jan-2025.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | ceqsexvOLD 3530* | Obsolete version of ceqsexv 3529 as of 12-Oct-2024. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2174. (Revised by GG, 12-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | ceqsexvOLDOLD 3531* | Obsolete version of ceqsexv 3529 as of 12-Oct-2024. (Contributed by NM, 2-Mar-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | ceqsexv2d 3532* | Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016.) Shorten, reduce dv conditions. (Revised by Wolf Lammen, 5-Jun-2025.) (Proof shortened by SN, 5-Jun-2025.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ ∃𝑥𝜑 | ||
Theorem | ceqsexv2dOLD 3533* | Obsolete version of ceqsexv2d 3532 as of 5-Jun-2025. (Contributed by Thierry Arnoux, 10-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ ∃𝑥𝜑 | ||
Theorem | ceqsex2 3534* | Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜒 & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑) ↔ 𝜒) | ||
Theorem | ceqsex2v 3535* | Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.) Avoid ax-10 2138 and ax-11 2154. (Revised by GG, 20-Aug-2023.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑) ↔ 𝜒) | ||
Theorem | ceqsex3v 3536* | Elimination of three existential quantifiers, using implicit substitution. (Contributed by NM, 16-Aug-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜑) ↔ 𝜃) | ||
Theorem | ceqsex4v 3537* | Elimination of four existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷) ∧ 𝜑) ↔ 𝜏) | ||
Theorem | ceqsex6v 3538* | Elimination of six existential quantifiers, using implicit substitution. (Contributed by NM, 21-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑣 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑢 = 𝐹 → (𝜂 ↔ 𝜁)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ (𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑) ↔ 𝜁) | ||
Theorem | ceqsex8v 3539* | Elimination of eight existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ 𝐺 ∈ V & ⊢ 𝐻 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑣 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑢 = 𝐹 → (𝜂 ↔ 𝜁)) & ⊢ (𝑡 = 𝐺 → (𝜁 ↔ 𝜎)) & ⊢ (𝑠 = 𝐻 → (𝜎 ↔ 𝜌)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢∃𝑡∃𝑠(((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ∧ ((𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ (𝑡 = 𝐺 ∧ 𝑠 = 𝐻)) ∧ 𝜑) ↔ 𝜌) | ||
Theorem | gencbvex 3540* | Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ 𝐴 ∈ V & ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃)) & ⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦)) ⇒ ⊢ (∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓)) | ||
Theorem | gencbvex2 3541* | Restatement of gencbvex 3540 with weaker hypotheses. (Contributed by Jeff Hankins, 6-Dec-2006.) |
⊢ 𝐴 ∈ V & ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃)) & ⊢ (𝜃 → ∃𝑥(𝜒 ∧ 𝐴 = 𝑦)) ⇒ ⊢ (∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓)) | ||
Theorem | gencbval 3542* | Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) |
⊢ 𝐴 ∈ V & ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃)) & ⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦)) ⇒ ⊢ (∀𝑥(𝜒 → 𝜑) ↔ ∀𝑦(𝜃 → 𝜓)) | ||
Theorem | sbhypf 3543* | Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf 3936. (Contributed by Raph Levien, 10-Apr-2004.) (Proof shortened by Wolf Lammen, 25-Jan-2025.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | sbhypfOLD 3544* | Obsolete version of sbhypf 3543 as of 25-Jan-2025. (Contributed by Raph Levien, 10-Apr-2004.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | spcimgft 3545 | Closed theorem form of spcimgf 3549. (Contributed by Wolf Lammen, 28-Jul-2025.) |
⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓))) → (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))) | ||
Theorem | spcimgfi1 3546 | A closed version of spcimgf 3549. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 27-Jul-2025.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓))) | ||
Theorem | spcimgfi1OLD 3547 | Obsolete version of spcimgfi1 3546 as of 27-Jul-2025. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓))) | ||
Theorem | spcgft 3548 | A closed version of spcgf 3590. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 4-Jan-2017.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓))) | ||
Theorem | spcimgf 3549 | Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | spcimegf 3550 | Existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) | ||
Theorem | vtoclgft 3551 | Closed theorem form of vtoclgf 3568. The reverse implication is proven in ceqsal1t 3511. See ceqsalt 3512 for a version with 𝑥 and 𝐴 disjoint. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by JJ, 11-Aug-2021.) Avoid ax-13 2374. (Revised by GG, 6-Oct-2023.) |
⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → 𝜓) | ||
Theorem | vtocleg 3552* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝑥 = 𝐴 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜑) | ||
Theorem | vtoclg 3553* | Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) Avoid ax-12 2174. (Revised by SN, 20-Apr-2024.) (Proof shortened by Wolf Lammen, 26-Jan-2025.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | vtocle 3554* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 9-Sep-1993.) Avoid df-clab 2712. (Revised by Wolf Lammen, 31-May-2025.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | vtocleOLD 3555* | Obsolete version of vtocle 3554 as of 31-May-2025. (Contributed by NM, 9-Sep-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | vtoclbg 3556* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃)) | ||
Theorem | vtocl 3557* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2138. (Revised by BJ, 29-Nov-2020.) (Proof shortened by SN, 20-Apr-2024.) (Proof shortened by Wolf Lammen, 20-Jun-2025.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | vtoclOLD 3558* | Obsolete version of vtocl 3557 as of 20-Jun-2025. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2138. (Revised by BJ, 29-Nov-2020.) (Proof shortened by SN, 20-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | vtocldf 3559 | Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜓) & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | vtocld 3560* | Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.) Avoid ax-10 2138, ax-11 2154, ax-12 2174. (Revised by SN, 2-Sep-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | vtocl2d 3561* | Implicit substitution of two classes for two setvar variables. (Contributed by Thierry Arnoux, 25-Aug-2020.) (Revised by BTernaryTau, 19-Oct-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | vtoclef 3562* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 18-Aug-1993.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | vtoclf 3563* | Implicit substitution of a class for a setvar variable. This is a generalization of chvar 2397. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Jan-2025.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | vtoclfOLD 3564* | Obsolete version of vtoclf 3563 as of 26-Jan-2025. (Contributed by NM, 30-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | vtocl2 3565* | Implicit substitution of classes for setvar variables. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | vtocl3 3566* | Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Avoid ax-10 2138 and ax-11 2154. (Revised by GG, 20-Aug-2023.) (Proof shortened by Wolf Lammen, 23-Aug-2023.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | vtoclb 3567* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 23-Dec-1993.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜒 ↔ 𝜃) | ||
Theorem | vtoclgf 3568 | Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | vtoclg1f 3569* | Version of vtoclgf 3568 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-10 2138 and ax-11 2154. (Contributed by BJ, 1-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | vtoclgOLD 3570* | Obsolete version of vtoclg 3553 as of 26-Jan-2025. (Contributed by NM, 17-Apr-1995.) Avoid ax-12 2174. (Revised by SN, 20-Apr-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | vtocl2gf 3571 | Implicit substitution of a class for a setvar variable. (Contributed by NM, 25-Apr-1995.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜒 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝜑 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) | ||
Theorem | vtocl3gf 3572 | Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑧𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑧𝐵 & ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜒 & ⊢ Ⅎ𝑧𝜃 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ 𝜑 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝜃) | ||
Theorem | vtocl2g 3573* | Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) Remove dependency on ax-10 2138, ax-11 2154, and ax-13 2374. (Revised by Steven Nguyen, 29-Nov-2022.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝜑 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) | ||
Theorem | vtocl3g 3574* | Implicit substitution of a class for a setvar variable. Version of vtocl3gf 3572 with disjoint variable conditions instead of nonfreeness hypotheses, requiring fewer axioms. (Contributed by GG, 3-Oct-2024.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ 𝜑 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝜃) | ||
Theorem | vtoclgaf 3575* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝜓) | ||
Theorem | vtoclga 3576* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2138 and ax-11 2154. (Revised by GG, 20-Aug-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝜓) | ||
Theorem | vtocl2ga 3577* | Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2138 and ax-11 2154. (Revised by GG, 20-Aug-2023.) (Proof shortened by Wolf Lammen, 23-Aug-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒) | ||
Theorem | vtocl2gaf 3578* | Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 10-Aug-2013.) (Proof shortened by Wolf Lammen, 31-May-2025.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜒 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒) | ||
Theorem | vtocl2gafOLD 3579* | Obsolete version of vtocl2gaf 3578 as of 31-May-2025. (Contributed by NM, 10-Aug-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜒 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒) | ||
Theorem | vtocl3gaf 3580* | Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 11-Oct-2016.) (Proof shortened by Wolf Lammen, 31-May-2025.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑧𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑧𝐵 & ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜒 & ⊢ Ⅎ𝑧𝜃 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → 𝜃) | ||
Theorem | vtocl3gafOLD 3581* | Obsolete version of vtocl3gaf 3580 as of 31-May-2025. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 11-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑧𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑧𝐵 & ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜒 & ⊢ Ⅎ𝑧𝜃 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → 𝜃) | ||
Theorem | vtocl3ga 3582* | Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 20-Aug-1995.) Reduce axiom usage. (Revised by GG, 3-Oct-2024.) (Proof shortened by Wolf Lammen, 31-May-2025.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑆) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑆) → 𝜃) | ||
Theorem | vtocl3gaOLD 3583* | Obsolete version of vtocl3ga 3582 as of 31-May-2025. (Contributed by NM, 20-Aug-1995.) Reduce axiom usage. (Revised by GG, 3-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑆) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑆) → 𝜃) | ||
Theorem | vtocl4g 3584* | Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜌)) & ⊢ (𝑤 = 𝐷 → (𝜌 ↔ 𝜃)) & ⊢ 𝜑 ⇒ ⊢ (((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇)) → 𝜃) | ||
Theorem | vtocl4ga 3585* | Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019.) (Proof shortened by Wolf Lammen, 31-May-2025.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜌)) & ⊢ (𝑤 = 𝐷 → (𝜌 ↔ 𝜃)) & ⊢ (((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇)) → 𝜑) ⇒ ⊢ (((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇)) → 𝜃) | ||
Theorem | vtocl4gaOLD 3586* | Obsolete version of vtocl4ga 3585 as of 31-May-2025. (Contributed by AV, 22-Jan-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜌)) & ⊢ (𝑤 = 𝐷 → (𝜌 ↔ 𝜃)) & ⊢ (((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇)) → 𝜑) ⇒ ⊢ (((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇)) → 𝜃) | ||
Theorem | vtoclegft 3587* | Implicit substitution of a class for a setvar variable. (Closed theorem version of vtoclef 3562.) (Contributed by NM, 7-Nov-2005.) (Revised by Mario Carneiro, 11-Oct-2016.) (Proof shortened by Wolf Lammen, 26-Jan-2025.) |
⊢ ((𝐴 ∈ 𝐵 ∧ Ⅎ𝑥𝜑 ∧ ∀𝑥(𝑥 = 𝐴 → 𝜑)) → 𝜑) | ||
Theorem | vtoclegftOLD 3588* | Obsolete version of vtoclegft 3587 as of 26-Jan-2025. (Contributed by NM, 7-Nov-2005.) (Revised by Mario Carneiro, 11-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝐵 ∧ Ⅎ𝑥𝜑 ∧ ∀𝑥(𝑥 = 𝐴 → 𝜑)) → 𝜑) | ||
Theorem | vtoclri 3589* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Nov-1994.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ∀𝑥 ∈ 𝐵 𝜑 ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝜓) | ||
Theorem | spcgf 3590 | Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 2-Feb-1997.) (Revised by Andrew Salmon, 12-Aug-2011.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | spcegf 3591 | Existential specialization, using implicit substitution. (Contributed by NM, 2-Feb-1997.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) | ||
Theorem | spcimdv 3592* | Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) Avoid ax-10 2138 and ax-11 2154. (Revised by GG, 20-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
Theorem | spcdv 3593* | Rule of specialization, using implicit substitution. Analogous to rspcdv 3613. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
Theorem | spcimedv 3594* | Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → (𝜒 → ∃𝑥𝜓)) | ||
Theorem | spcgv 3595* | Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.) Avoid ax-10 2138, ax-11 2154. (Revised by Wolf Lammen, 25-Aug-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | spcegv 3596* | Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2138, ax-11 2154. (Revised by Wolf Lammen, 25-Aug-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) | ||
Theorem | spcedv 3597* | Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12-Aug-2020.) (Revised by AV, 16-Aug-2024.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝜒) & ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | spc2egv 3598* | Existential specialization with two quantifiers, using implicit substitution. (Contributed by NM, 3-Aug-1995.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝜓 → ∃𝑥∃𝑦𝜑)) | ||
Theorem | spc2gv 3599* | Specialization with two quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥∀𝑦𝜑 → 𝜓)) | ||
Theorem | spc2ed 3600* | Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.) |
⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑦𝜒 & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (𝜒 → ∃𝑥∃𝑦𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |