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