![]() |
Metamath
Proof Explorer Theorem List (p. 39 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sbccow 3801* | A composition law for class substitution. Version of sbcco 3804 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 26-Sep-2003.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ ([𝐴 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑) | ||
Theorem | nfsbcd 3802 | Deduction version of nfsbc 3803. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfsbcdw 3799 when possible. (Contributed by NM, 23-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥[𝐴 / 𝑦]𝜓) | ||
Theorem | nfsbc 3803 | Bound-variable hypothesis builder for class substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfsbcw 3800 when possible. (Contributed by NM, 7-Sep-2014.) (Revised by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑 | ||
Theorem | sbcco 3804* | A composition law for class substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker sbccow 3801 when possible. (Contributed by NM, 26-Sep-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) (New usage is discouraged.) |
⊢ ([𝐴 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑) | ||
Theorem | sbcco2 3805* | A composition law for class substitution. Importantly, 𝑥 may occur free in the class expression substituted for 𝐴. (Contributed by NM, 5-Sep-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ ([𝑥 / 𝑦][𝐵 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑) | ||
Theorem | sbc5 3806* | An equivalence for class substitution. (Contributed by NM, 23-Aug-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by SN, 2-Sep-2024.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) | ||
Theorem | sbc5ALT 3807* | Alternate proof of sbc5 3806. This proof helps show how clelab 2880 works, since it is equivalent but shorter thanks to now-available library theorems like vtoclbg 3560 and isset 3488. (Contributed by NM, 23-Aug-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) | ||
Theorem | sbc6g 3808* | An equivalence for class substitution. (Contributed by NM, 11-Oct-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Proof shortened by SN, 5-Oct-2024.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))) | ||
Theorem | sbc6gOLD 3809* | Obsolete version of sbc6g 3808 as of 5-Oct-2024. (Contributed by NM, 11-Oct-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))) | ||
Theorem | sbc6 3810* | An equivalence for class substitution. (Contributed by NM, 23-Aug-1993.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)) | ||
Theorem | sbc7 3811* | An equivalence for class substitution in the spirit of df-clab 2711. Note that 𝑥 and 𝐴 don't have to be distinct. (Contributed by NM, 18-Nov-2008.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝐴 ∧ [𝑦 / 𝑥]𝜑)) | ||
Theorem | cbvsbcw 3812* | Change bound variables in a wff substitution. Version of cbvsbc 3814 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Jeff Hankins, 19-Sep-2009.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑦]𝜓) | ||
Theorem | cbvsbcvw 3813* | Change the bound variable of a class substitution using implicit substitution. Version of cbvsbcv 3815 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 30-Sep-2008.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑦]𝜓) | ||
Theorem | cbvsbc 3814 | Change bound variables in a wff substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvsbcw 3812 when possible. (Contributed by Jeff Hankins, 19-Sep-2009.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑦]𝜓) | ||
Theorem | cbvsbcv 3815* | Change the bound variable of a class substitution using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvsbcvw 3813 when possible. (Contributed by NM, 30-Sep-2008.) (Revised by Mario Carneiro, 13-Oct-2016.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑦]𝜓) | ||
Theorem | sbciegft 3816* | Conversion of implicit substitution to explicit class substitution, using a bound-variable hypothesis instead of distinct variables. (Closed theorem version of sbciegf 3817.) (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | sbciegf 3817* | Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | sbcieg 3818* | Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.) Avoid ax-10 2138, ax-12 2172. (Revised by Gino Giotto, 12-Oct-2024.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | sbciegOLD 3819* | Obsolete version of sbcieg 3818 as of 12-Oct-2024. (Contributed by NM, 10-Nov-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | sbcie2g 3820* | Conversion of implicit substitution to explicit class substitution. This version of sbcie 3821 avoids a disjointness condition on 𝑥, 𝐴 by substituting twice. (Contributed by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜒)) | ||
Theorem | sbcie 3821* | Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | sbciedf 3822* | Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 29-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | sbcied 3823* | Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.) Avoid ax-10 2138, ax-12 2172. (Revised by Gino Giotto, 12-Oct-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | sbciedOLD 3824* | Obsolete version of sbcied 3823 as of 12-Oct-2024. (Contributed by NM, 13-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | sbcied2 3825* | Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | elrabsf 3826 | Membership in a restricted class abstraction, expressed with explicit class substitution. (The variation elrabf 3680 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 | eqsbc1 3827* | Substitution for the left-hand side in an equality. Class version of eqsb1 2860. (Contributed by Andrew Salmon, 29-Jun-2011.) Avoid ax-13 2372. (Revised by Wolf Lammen, 29-Apr-2023.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | sbcng 3828 | Move negation in and out of class substitution. (Contributed by NM, 16-Jan-2004.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ [𝐴 / 𝑥]𝜑)) | ||
Theorem | sbcimg 3829 | Distribution of class substitution over implication. (Contributed by NM, 16-Jan-2004.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))) | ||
Theorem | sbcan 3830 | Distribution of class substitution over conjunction. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 17-Aug-2018.) |
⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓)) | ||
Theorem | sbcor 3831 | Distribution of class substitution over disjunction. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 17-Aug-2018.) |
⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓)) | ||
Theorem | sbcbig 3832 | Distribution of class substitution over biconditional. (Contributed by Raph Levien, 10-Apr-2004.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) | ||
Theorem | sbcn1 3833 | Move negation in and out of class substitution. One direction of sbcng 3828 that holds for proper classes. (Contributed by NM, 17-Aug-2018.) |
⊢ ([𝐴 / 𝑥] ¬ 𝜑 → ¬ [𝐴 / 𝑥]𝜑) | ||
Theorem | sbcim1 3834 | Distribution of class substitution over implication. One direction of sbcimg 3829 that holds for proper classes. (Contributed by NM, 17-Aug-2018.) Avoid ax-10 2138, ax-12 2172. (Revised by SN, 26-Oct-2024.) |
⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)) | ||
Theorem | sbcim1OLD 3835 | Obsolete version of sbcim1 3834 as of 26-Oct-2024. (Contributed by NM, 17-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)) | ||
Theorem | sbcbid 3836 | Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) | ||
Theorem | sbcbidv 3837* | Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014.) Drop ax-12 2172. (Revised by Gino Giotto, 1-Dec-2023.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) | ||
Theorem | sbcbii 3838 | Formula-building inference for class substitution. (Contributed by NM, 11-Nov-2005.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) | ||
Theorem | sbcbi1 3839 | Distribution of class substitution over biconditional. One direction of sbcbig 3832 that holds for proper classes. (Contributed by NM, 17-Aug-2018.) |
⊢ ([𝐴 / 𝑥](𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) | ||
Theorem | sbcbi2 3840 | Substituting into equivalent wff's gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.) (Proof shortened by Wolf Lammen, 4-May-2023.) Avoid ax-10, ax-12. (Revised by Steven Nguyen, 5-May-2024.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) | ||
Theorem | sbcbi2OLD 3841 | Obsolete proof of sbcbi2 3840 as of 5-May-2024. (Contributed by Giovanni Mascellani, 9-Apr-2018.) (Proof shortened by Wolf Lammen, 4-May-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) | ||
Theorem | sbcal 3842* | Move universal quantifier in and out of class substitution. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝐴 / 𝑦]𝜑) | ||
Theorem | sbcex2 3843* | Move existential quantifier in and out of class substitution. (Contributed by NM, 21-May-2004.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑) | ||
Theorem | sbceqal 3844* | Class version of one implication of equvelv 2035. (Contributed by Andrew Salmon, 28-Jun-2011.) (Proof shortened by SN, 26-Oct-2024.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝑥 = 𝐵) → 𝐴 = 𝐵)) | ||
Theorem | sbceqalOLD 3845* | Obsolete version of sbceqal 3844 as of 26-Oct-2024. (Contributed by Andrew Salmon, 28-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝑥 = 𝐵) → 𝐴 = 𝐵)) | ||
Theorem | sbeqalb 3846* | Theorem *14.121 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 28-Jun-2011.) (Proof shortened by Wolf Lammen, 9-May-2013.) |
⊢ (𝐴 ∈ 𝑉 → ((∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ∧ ∀𝑥(𝜑 ↔ 𝑥 = 𝐵)) → 𝐴 = 𝐵)) | ||
Theorem | eqsbc2 3847* | Substitution for the right-hand side in an equality. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by JJ, 7-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝑥 ↔ 𝐵 = 𝐴)) | ||
Theorem | sbc3an 3848 | Distribution of class substitution over triple conjunction. (Contributed by NM, 14-Dec-2006.) (Revised by NM, 17-Aug-2018.) |
⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓 ∧ [𝐴 / 𝑥]𝜒)) | ||
Theorem | sbcel1v 3849* | Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.) Avoid ax-13 2372. (Revised by Wolf Lammen, 30-Apr-2023.) |
⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵) | ||
Theorem | sbcel2gv 3850* | Class substitution into a membership relation. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐵 ∈ 𝑉 → ([𝐵 / 𝑥]𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | sbcel21v 3851* | Class substitution into a membership relation. One direction of sbcel2gv 3850 that holds for proper classes. (Contributed by NM, 17-Aug-2018.) |
⊢ ([𝐵 / 𝑥]𝐴 ∈ 𝑥 → 𝐴 ∈ 𝐵) | ||
Theorem | sbcimdv 3852* | Substitution analogue of Theorem 19.20 of [Margaris] p. 90 (alim 1813). (Contributed by NM, 11-Nov-2005.) (Revised by NM, 17-Aug-2018.) (Proof shortened by JJ, 7-Jul-2021.) Reduce axiom usage. (Revised by Gino Giotto, 12-Oct-2024.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) | ||
Theorem | sbcimdvOLD 3853* | Obsolete version of sbcimdv 3852 as of 12-Oct-2024. (Contributed by NM, 11-Nov-2005.) (Revised by NM, 17-Aug-2018.) (Proof shortened by JJ, 7-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) | ||
Theorem | sbctt 3854 | Substitution for a variable not free in a wff does not affect it. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝜑) → ([𝐴 / 𝑥]𝜑 ↔ 𝜑)) | ||
Theorem | sbcgf 3855 | 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 3856 | Substitution for a variable not free in antecedent affects only the consequent. (Contributed by NM, 11-Oct-2004.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝐴 / 𝑥]𝜓))) | ||
Theorem | sbcg 3857* | Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3855. (Contributed by Alan Sare, 10-Nov-2012.) Reduce axiom usage. (Revised by Gino Giotto, 12-Oct-2024.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑)) | ||
Theorem | sbcgOLD 3858* | Obsolete version of sbcg 3857 as of 12-Oct-2024. (Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑)) | ||
Theorem | sbcgfi 3859 | 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 3860* | Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ Ⅎ𝑥 𝐵 ∈ 𝑊 & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ 𝜓)) | ||
Theorem | sbc2ie 3861* | Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008.) (Revised by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Gino Giotto, 12-Oct-2024.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ 𝜓) | ||
Theorem | sbc2ieOLD 3862* | Obsolete version of sbc2ie 3861 as of 12-Oct-2024. (Contributed by NM, 16-Dec-2008.) (Revised by Mario Carneiro, 19-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ 𝜓) | ||
Theorem | sbc2iedv 3863* | 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 3864* | 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 3865* | Lemma for sbccom 3866. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.) |
⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
Theorem | sbccom 3866* | Commutative law for double class substitution. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Mario Carneiro, 18-Oct-2016.) |
⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
Theorem | sbcralt 3867* | Interchange class substitution and restricted quantifier. (Contributed by NM, 1-Mar-2008.) (Revised by David Abernethy, 22-Feb-2010.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) | ||
Theorem | sbcrext 3868* | 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 3869* | Interchange class substitution and restricted quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) | ||
Theorem | sbcrex 3870* | Interchange class substitution and restricted existential quantifier. (Contributed by NM, 15-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑) | ||
Theorem | sbcreu 3871* | Interchange class substitution and restricted unique existential quantifier. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑) | ||
Theorem | reu8nf 3872* | Restricted uniqueness using implicit substitution. This version of reu8 3730 uses a nonfreeness hypothesis for 𝑥 and 𝜓 instead of distinct variable conditions. (Contributed by AV, 21-Jan-2022.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒)) & ⊢ (𝑤 = 𝑦 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) | ||
Theorem | sbcabel 3873* | Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]{𝑦 ∣ 𝜑} ∈ 𝐵 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝜑} ∈ 𝐵)) | ||
Theorem | rspsbc 3874* | 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 2072 and spsbc 3791. See also rspsbca 3875 and rspcsbela 4436. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) |
⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → [𝐴 / 𝑥]𝜑)) | ||
Theorem | rspsbca 3875* | Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. (Contributed by NM, 14-Dec-2005.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → [𝐴 / 𝑥]𝜑) | ||
Theorem | rspesbca 3876* | Existence form of rspsbca 3875. (Contributed by NM, 29-Feb-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) |
⊢ ((𝐴 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝜑) → ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | spesbc 3877 | Existence form of spsbc 3791. (Contributed by Mario Carneiro, 18-Nov-2016.) |
⊢ ([𝐴 / 𝑥]𝜑 → ∃𝑥𝜑) | ||
Theorem | spesbcd 3878 | form of spsbc 3791. (Contributed by Mario Carneiro, 9-Feb-2017.) |
⊢ (𝜑 → [𝐴 / 𝑥]𝜓) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | sbcth2 3879* | A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.) |
⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝐵 → [𝐴 / 𝑥]𝜑) | ||
Theorem | ra4v 3880* | Version of ra4 3881 with a disjoint variable condition, requiring fewer axioms. This is stdpc5v 1942 for a restricted domain. (Contributed by BJ, 27-Mar-2020.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | ra4 3881 | Restricted quantifier version of Axiom 5 of [Mendelson] p. 69. This is the axiom stdpc5 2202 of standard predicate calculus for a restricted domain. See ra4v 3880 for a version requiring fewer axioms. (Contributed by NM, 16-Jan-2004.) (Proof shortened by BJ, 27-Mar-2020.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | rmo2 3882* | Alternate definition of restricted "at most one". Note that ∃*𝑥 ∈ 𝐴𝜑 is not equivalent to ∃𝑦 ∈ 𝐴∀𝑥 ∈ 𝐴(𝜑 → 𝑥 = 𝑦) (in analogy to reu6 3723); to see this, let 𝐴 be the empty set. However, one direction of this pattern holds; see rmo2i 3883. (Contributed by NM, 17-Jun-2017.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) | ||
Theorem | rmo2i 3883* | Condition implying restricted "at most one". (Contributed by NM, 17-Jun-2017.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) → ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rmo3 3884* | Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) Avoid ax-13 2372. (Revised by Wolf Lammen, 30-Apr-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) | ||
Theorem | rmob 3885* | Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((∃*𝑥 ∈ 𝐴 𝜑 ∧ (𝐵 ∈ 𝐴 ∧ 𝜓)) → (𝐵 = 𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝜒))) | ||
Theorem | rmoi 3886* | Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((∃*𝑥 ∈ 𝐴 𝜑 ∧ (𝐵 ∈ 𝐴 ∧ 𝜓) ∧ (𝐶 ∈ 𝐴 ∧ 𝜒)) → 𝐵 = 𝐶) | ||
Theorem | rmob2 3887* | Consequence of "restricted at most one". (Contributed by Thierry Arnoux, 9-Dec-2019.) |
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝑥 = 𝐵 ↔ 𝜒)) | ||
Theorem | rmoi2 3888* | Consequence of "restricted at most one". (Contributed by Thierry Arnoux, 9-Dec-2019.) |
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → 𝑥 = 𝐵) | ||
Theorem | rmoanim 3889 | Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim 2617. (Contributed by Alexander van der Vekens, 25-Jun-2017.) Avoid ax-10 2138 and ax-11 2155. (Revised by Gino Giotto, 24-Aug-2023.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | rmoanimALT 3890 | Alternate proof of rmoanim 3889, shorter but requiring ax-10 2138 and ax-11 2155. (Contributed by Alexander van der Vekens, 25-Jun-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | reuan 3891 | Introduction of a conjunct into restricted unique existential quantifier, analogous to euan 2618. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃!𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | 2reu1 3892* | Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 2647. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
⊢ (∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) | ||
Theorem | 2reu2 3893* | Double restricted existential uniqueness, analogous to 2eu2 2649. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
⊢ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)) | ||
Syntax | csb 3894 | Extend class notation to include the proper substitution of a class for a set into another class. |
class ⦋𝐴 / 𝑥⦌𝐵 | ||
Definition | df-csb 3895* | 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 3778, to prevent ambiguity. Theorem sbcel1g 4414 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 4407). Theorem sbccsb 4434 recovers substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.) |
⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | ||
Theorem | csb2 3896* | 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 3897 | Analogue of dfsbcq 3780 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) | ||
Theorem | csbeq1d 3898 | Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) | ||
Theorem | csbeq2 3899 | Substituting into equivalent classes gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.) |
⊢ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | csbeq2d 3900 | Formula-building deduction for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |