![]() |
Metamath
Proof Explorer Theorem List (p. 38 of 444) | < 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-28489) |
![]() (28490-30014) |
![]() (30015-44305) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sbc6 3701* | An equivalence for class substitution. (Contributed by NM, 23-Aug-1993.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)) | ||
Theorem | sbc7 3702* | An equivalence for class substitution in the spirit of df-clab 2752. Note that 𝑥 and 𝐴 don't have to be distinct. (Contributed by NM, 18-Nov-2008.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝐴 ∧ [𝑦 / 𝑥]𝜑)) | ||
Theorem | cbvsbc 3703 | Change bound variables in a wff substitution. (Contributed by Jeff Hankins, 19-Sep-2009.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑦]𝜓) | ||
Theorem | cbvsbcv 3704* | Change the bound variable of a class substitution using implicit substitution. (Contributed by NM, 30-Sep-2008.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑦]𝜓) | ||
Theorem | sbciegft 3705* | Conversion of implicit substitution to explicit class substitution, using a bound-variable hypothesis instead of distinct variables. (Closed theorem version of sbciegf 3706.) (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | sbciegf 3706* | Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | sbcieg 3707* | Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | sbcie2g 3708* | Conversion of implicit substitution to explicit class substitution. This version of sbcie 3709 avoids a disjointness condition on 𝑥, 𝐴 by substituting twice. (Contributed by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜒)) | ||
Theorem | sbcie 3709* | Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | sbciedf 3710* | Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 29-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | sbcied 3711* | Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | sbcied2 3712* | Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | elrabsf 3713 | Membership in a restricted class abstraction, expressed with explicit class substitution. (The variation elrabf 3584 has implicit substitution). The hypothesis specifies that 𝑥 must not be a free variable in 𝐵. (Contributed by NM, 30-Sep-2003.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑)) | ||
Theorem | eqsbc3 3714* | Substitution applied to an atomic wff. Class version of eqsb3 2885. (Contributed by Andrew Salmon, 29-Jun-2011.) Avoid ax-13 2302. (Revised by Wolf Lammen, 29-Apr-2023.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | eqsbc3OLD 3715* | Obsolete version of eqsbc3 3714 as of 29-Apr-2023. (Contributed by Andrew Salmon, 29-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | sbcng 3716 | Move negation in and out of class substitution. (Contributed by NM, 16-Jan-2004.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ [𝐴 / 𝑥]𝜑)) | ||
Theorem | sbcimg 3717 | Distribution of class substitution over implication. (Contributed by NM, 16-Jan-2004.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))) | ||
Theorem | sbcan 3718 | Distribution of class substitution over conjunction. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 17-Aug-2018.) |
⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓)) | ||
Theorem | sbcor 3719 | Distribution of class substitution over disjunction. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 17-Aug-2018.) |
⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓)) | ||
Theorem | sbcbig 3720 | Distribution of class substitution over biconditional. (Contributed by Raph Levien, 10-Apr-2004.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) | ||
Theorem | sbcn1 3721 | Move negation in and out of class substitution. One direction of sbcng 3716 that holds for proper classes. (Contributed by NM, 17-Aug-2018.) |
⊢ ([𝐴 / 𝑥] ¬ 𝜑 → ¬ [𝐴 / 𝑥]𝜑) | ||
Theorem | sbcim1 3722 | Distribution of class substitution over implication. One direction of sbcimg 3717 that holds for proper classes. (Contributed by NM, 17-Aug-2018.) |
⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)) | ||
Theorem | sbcbid 3723 | Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) | ||
Theorem | sbcbidv 3724* | Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) | ||
Theorem | sbcbii 3725 | Formula-building inference for class substitution. (Contributed by NM, 11-Nov-2005.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) | ||
Theorem | sbcbi1 3726 | Distribution of class substitution over biconditional. One direction of sbcbig 3720 that holds for proper classes. (Contributed by NM, 17-Aug-2018.) |
⊢ ([𝐴 / 𝑥](𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) | ||
Theorem | sbcbi2 3727 | Substituting into equivalent wff's gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.) (Proof shortened by Wolf Lammen, 4-May-2023.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) | ||
Theorem | sbcbi2OLD 3728 | Obsolete proof of sbcbi2 3727 as of 4-May-2023. (Contributed by Giovanni Mascellani, 9-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) | ||
Theorem | sbcal 3729* | Move universal quantifier in and out of class substitution. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝐴 / 𝑦]𝜑) | ||
Theorem | sbcex2 3730* | Move existential quantifier in and out of class substitution. (Contributed by NM, 21-May-2004.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑) | ||
Theorem | sbceqal 3731* | Class version of one implication of equvelv 1989. (Contributed by Andrew Salmon, 28-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝑥 = 𝐵) → 𝐴 = 𝐵)) | ||
Theorem | sbeqalb 3732* | Theorem *14.121 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 28-Jun-2011.) (Proof shortened by Wolf Lammen, 9-May-2013.) |
⊢ (𝐴 ∈ 𝑉 → ((∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ∧ ∀𝑥(𝜑 ↔ 𝑥 = 𝐵)) → 𝐴 = 𝐵)) | ||
Theorem | eqsbc3r 3733* | eqsbc3 3714 with setvar variable on right side of equals sign. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by JJ, 7-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝑥 ↔ 𝐵 = 𝐴)) | ||
Theorem | sbc3an 3734 | Distribution of class substitution over triple conjunction. (Contributed by NM, 14-Dec-2006.) (Revised by NM, 17-Aug-2018.) |
⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓 ∧ [𝐴 / 𝑥]𝜒)) | ||
Theorem | sbcel1v 3735* | Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.) Avoid ax-13 2302. (Revised by Wolf Lammen, 30-Apr-2023.) |
⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵) | ||
Theorem | sbcel1vOLD 3736* | Obsolete version of sbcel1v 3735 as of 30-Apr-2023. (Contributed by NM, 17-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵) | ||
Theorem | sbcel2gv 3737* | Class substitution into a membership relation. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐵 ∈ 𝑉 → ([𝐵 / 𝑥]𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | sbcel21v 3738* | Class substitution into a membership relation. One direction of sbcel2gv 3737 that holds for proper classes. (Contributed by NM, 17-Aug-2018.) |
⊢ ([𝐵 / 𝑥]𝐴 ∈ 𝑥 → 𝐴 ∈ 𝐵) | ||
Theorem | sbcimdv 3739* | Substitution analogue of Theorem 19.20 of [Margaris] p. 90 (alim 1774). (Contributed by NM, 11-Nov-2005.) (Revised by NM, 17-Aug-2018.) (Proof shortened by JJ, 7-Jul-2021.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) | ||
Theorem | sbctt 3740 | Substitution for a variable not free in a wff does not affect it. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝜑) → ([𝐴 / 𝑥]𝜑 ↔ 𝜑)) | ||
Theorem | sbcgf 3741 | Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 11-Oct-2004.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑)) | ||
Theorem | sbc19.21g 3742 | Substitution for a variable not free in antecedent affects only the consequent. (Contributed by NM, 11-Oct-2004.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝐴 / 𝑥]𝜓))) | ||
Theorem | sbcg 3743* | Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3741. (Contributed by Alan Sare, 10-Nov-2012.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑)) | ||
Theorem | sbcgfi 3744 | Substitution for a variable not free in a wff does not affect it, in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.) |
⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | sbc2iegf 3745* | Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ Ⅎ𝑥 𝐵 ∈ 𝑊 & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ 𝜓)) | ||
Theorem | sbc2ie 3746* | Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ 𝜓) | ||
Theorem | sbc2iedv 3747* | Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008.) (Proof shortened by Mario Carneiro, 18-Oct-2016.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜓 ↔ 𝜒)) | ||
Theorem | sbc3ie 3748* | Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Jun-2014.) (Revised by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦][𝐶 / 𝑧]𝜑 ↔ 𝜓) | ||
Theorem | sbccomlem 3749* | Lemma for sbccom 3750. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.) |
⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
Theorem | sbccom 3750* | Commutative law for double class substitution. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Mario Carneiro, 18-Oct-2016.) |
⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
Theorem | sbcralt 3751* | Interchange class substitution and restricted quantifier. (Contributed by NM, 1-Mar-2008.) (Revised by David Abernethy, 22-Feb-2010.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) | ||
Theorem | sbcrext 3752* | Interchange class substitution and restricted existential quantifier. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) (Revised by NM, 18-Aug-2018.) (Proof shortened by JJ, 7-Jul-2021.) |
⊢ (Ⅎ𝑦𝐴 → ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) | ||
Theorem | sbcralg 3753* | Interchange class substitution and restricted quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) | ||
Theorem | sbcrex 3754* | Interchange class substitution and restricted existential quantifier. (Contributed by NM, 15-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑) | ||
Theorem | sbcreu 3755* | Interchange class substitution and restricted unique existential quantifier. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑) | ||
Theorem | reu8nf 3756* | Restricted uniqueness using implicit substitution. This version of reu8 3629 uses a non-freeness hypothesis for 𝑥 and 𝜓 instead of distinct variable conditions. (Contributed by AV, 21-Jan-2022.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒)) & ⊢ (𝑤 = 𝑦 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) | ||
Theorem | sbcabel 3757* | Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]{𝑦 ∣ 𝜑} ∈ 𝐵 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝜑} ∈ 𝐵)) | ||
Theorem | rspsbc 3758* | Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. This provides an axiom for a predicate calculus for a restricted domain. This theorem generalizes the unrestricted stdpc4 2020 and spsbc 3687. See also rspsbca 3759 and rspcsbela 4265. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) |
⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → [𝐴 / 𝑥]𝜑)) | ||
Theorem | rspsbca 3759* | Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. (Contributed by NM, 14-Dec-2005.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → [𝐴 / 𝑥]𝜑) | ||
Theorem | rspesbca 3760* | Existence form of rspsbca 3759. (Contributed by NM, 29-Feb-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) |
⊢ ((𝐴 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑) → ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | spesbc 3761 | Existence form of spsbc 3687. (Contributed by Mario Carneiro, 18-Nov-2016.) |
⊢ ([𝐴 / 𝑥]𝜑 → ∃𝑥𝜑) | ||
Theorem | spesbcd 3762 | form of spsbc 3687. (Contributed by Mario Carneiro, 9-Feb-2017.) |
⊢ (𝜑 → [𝐴 / 𝑥]𝜓) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | sbcth2 3763* | A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) |
⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝐵 → [𝐴 / 𝑥]𝜑) | ||
Theorem | ra4v 3764* | Version of ra4 3765 with a disjoint variable condition, requiring fewer axioms. This is stdpc5v 1898 for a restricted domain. (Contributed by BJ, 27-Mar-2020.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | ra4 3765 | Restricted quantifier version of Axiom 5 of [Mendelson] p. 69. This is the axiom stdpc5 2138 of standard predicate calculus for a restricted domain. See ra4v 3764 for a version requiring fewer axioms. (Contributed by NM, 16-Jan-2004.) (Proof shortened by BJ, 27-Mar-2020.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | rmo2 3766* | Alternate definition of restricted "at most one." Note that ∃*𝑥 ∈ 𝐴𝜑 is not equivalent to ∃𝑦 ∈ 𝐴∀𝑥 ∈ 𝐴(𝜑 → 𝑥 = 𝑦) (in analogy to reu6 3622); to see this, let 𝐴 be the empty set. However, one direction of this pattern holds; see rmo2i 3767. (Contributed by NM, 17-Jun-2017.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) | ||
Theorem | rmo2i 3767* | Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) → ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rmo3 3768* | Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) Avoid ax-13 2302. (Revised by Wolf Lammen, 30-Apr-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) | ||
Theorem | rmo3OLD 3769* | Obsolete version of rmo3 3768 as of 30-Apr-2023. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) | ||
Theorem | rmob 3770* | Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((∃*𝑥 ∈ 𝐴 𝜑 ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒))) | ||
Theorem | rmoi 3771* | Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((∃*𝑥 ∈ 𝐴 𝜑 ∧ (𝐵 ∈ 𝐴 ∧ 𝜓) ∧ (𝐶 ∈ 𝐴 ∧ 𝜒)) → 𝐵 = 𝐶) | ||
Theorem | rmob2 3772* | Consequence of "restricted at most one." (Contributed by Thierry Arnoux, 9-Dec-2019.) |
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝑥 = 𝐵 ↔ 𝜒)) | ||
Theorem | rmoi2 3773* | Consequence of "restricted at most one." (Contributed by Thierry Arnoux, 9-Dec-2019.) |
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → 𝑥 = 𝐵) | ||
Theorem | rmoanim 3774* | Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim 2653. (Contributed by Alexander van der Vekens, 25-Jun-2017.) Avoid ax-10 2080 and ax-11 2094. (Revised by Gino Giotto, 24-Aug-2023.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | rmoanimALT 3775* | Alternate proof of rmoanim 3774, shorter but requiring ax-10 2080 and ax-11 2094. (Contributed by Alexander van der Vekens, 25-Jun-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | reuan 3776* | Introduction of a conjunct into restricted unique existential quantifier, analogous to euan 2654. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃!𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | 2reu1 3777* | Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 2681. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
⊢ (∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) | ||
Theorem | 2reu2 3778* | Double restricted existential uniqueness, analogous to 2eu2 2683. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
⊢ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)) | ||
Syntax | csb 3779 | Extend class notation to include the proper substitution of a class for a set into another class. |
class ⦋𝐴 / 𝑥⦌𝐵 | ||
Definition | df-csb 3780* | Define the proper substitution of a class for a set into another class. The underlined brackets distinguish it from the substitution into a wff, wsbc 3674, to prevent ambiguity. Theorem sbcel1g 4245 shows an example of how ambiguity could arise if we did not use distinguished brackets. When 𝐴 is a proper class, this evaluates to the empty set (see csbprc 4238). Theorem sbccsb 4263 recovers substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.) |
⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | ||
Theorem | csb2 3781* | Alternate expression for the proper substitution into a class, without referencing substitution into a wff. Note that 𝑥 can be free in 𝐵 but cannot occur in 𝐴. (Contributed by NM, 2-Dec-2013.) |
⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ ∃𝑥(𝑥 = 𝐴 ∧ 𝑦 ∈ 𝐵)} | ||
Theorem | csbeq1 3782 | Analogue of dfsbcq 3676 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) | ||
Theorem | csbeq2 3783 | Substituting into equivalent classes gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.) |
⊢ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | cbvcsb 3784 | Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on 𝐴. (Contributed by Jeff Hankins, 13-Sep-2009.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑦⦌𝐷 | ||
Theorem | cbvcsbv 3785* | Change the bound variable of a proper substitution into a class using implicit substitution. (Contributed by NM, 30-Sep-2008.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑦⦌𝐶 | ||
Theorem | csbeq1d 3786 | Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) | ||
Theorem | csbid 3787 | Analogue of sbid 2184 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 | ||
Theorem | csbeq1a 3788 | Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵) | ||
Theorem | csbco 3789* | Composition law for chained substitutions into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | csbtt 3790 | Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐵) → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | csbconstgf 3791 | Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by NM, 10-Nov-2005.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | csbconstg 3792* | Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3791 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | csbgfi 3793 | Substitution for a variable not free in a class does not affect it, in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.) |
⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐵 | ||
Theorem | csbconstgi 3794* | The proper substitution of a class for a variable in another variable does not modify it, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝑦 = 𝑦 | ||
Theorem | nfcsb1d 3795 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) | ||
Theorem | nfcsb1 3796 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | nfcsb1v 3797* | Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | nfcsbd 3798 | Deduction version of nfcsb 3799. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵) | ||
Theorem | nfcsb 3799 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 | ||
Theorem | csbhypf 3800* | Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 3466 for class substitution version. (Contributed by NM, 19-Dec-2008.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |