![]() |
Metamath
Proof Explorer Theorem List (p. 40 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 | rmoi2 3901* | Consequence of "restricted at most one". (Contributed by Thierry Arnoux, 9-Dec-2019.) |
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → 𝑥 = 𝐵) | ||
Theorem | rmoanim 3902 | 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 2154. (Revised by GG, 24-Aug-2023.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | rmoanimALT 3903 | Alternate proof of rmoanim 3902, shorter but requiring ax-10 2138 and ax-11 2154. (Contributed by Alexander van der Vekens, 25-Jun-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | reuan 3904 | Introduction of a conjunct into restricted unique existential quantifier, analogous to euan 2618. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃!𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | 2reu1 3905* | Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 2648. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
⊢ (∀𝑥 ∈ 𝐴 ∃*𝑦 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) | ||
Theorem | 2reu2 3906* | Double restricted existential uniqueness, analogous to 2eu2 2650. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
⊢ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 → (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)) | ||
Syntax | csb 3907 | Extend class notation to include the proper substitution of a class for a set into another class. |
class ⦋𝐴 / 𝑥⦌𝐵 | ||
Definition | df-csb 3908* | 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 3790, to prevent ambiguity. Theorem sbcel1g 4421 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 4414). Theorem sbccsb 4441 recovers substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.) |
⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | ||
Theorem | csb2 3909* | 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 3910 | Analogue of dfsbcq 3792 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) | ||
Theorem | csbeq1d 3911 | Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) | ||
Theorem | csbeq2 3912 | Substituting into equivalent classes gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.) |
⊢ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | csbeq2d 3913 | Formula-building deduction for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | csbeq2dv 3914* | Formula-building deduction for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | csbeq2i 3915 | Formula-building inference for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 | ||
Theorem | csbeq12dv 3916* | Formula-building inference for class substitution. (Contributed by SN, 3-Nov-2023.) |
⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐷) | ||
Theorem | cbvcsbw 3917* | Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on 𝐴. Version of cbvcsb 3918 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by Jeff Hankins, 13-Sep-2009.) Avoid ax-13 2374. (Revised by GG, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑦⦌𝐷 | ||
Theorem | cbvcsb 3918 | Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on 𝐴. Usage of this theorem is discouraged because it depends on ax-13 2374. Use the weaker cbvcsbw 3917 when possible. (Contributed by Jeff Hankins, 13-Sep-2009.) (Revised by Mario Carneiro, 11-Dec-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑦⦌𝐷 | ||
Theorem | cbvcsbv 3919* | 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 | csbid 3920 | Analogue of sbid 2252 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 | ||
Theorem | csbeq1a 3921 | Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵) | ||
Theorem | csbcow 3922* | Composition law for chained substitutions into a class. Version of csbco 3923 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by NM, 10-Nov-2005.) Avoid ax-13 2374. (Revised by GG, 10-Jan-2024.) |
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | csbco 3923* | Composition law for chained substitutions into a class. Usage of this theorem is discouraged because it depends on ax-13 2374. Use the weaker csbcow 3922 when possible. (Contributed by NM, 10-Nov-2005.) (New usage is discouraged.) |
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | csbtt 3924 | Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐵) → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | csbconstgf 3925 | Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by NM, 10-Nov-2005.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | csbconstg 3926* | Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3925 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2174. (Revised by GG, 15-Oct-2024.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | csbconstgOLD 3927* | Obsolete version of csbconstg 3926 as of 15-Oct-2024. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | csbgfi 3928 | 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 3929* | 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 3930 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) | ||
Theorem | nfcsb1 3931 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | nfcsb1v 3932* | Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | nfcsbd 3933 | Deduction version of nfcsb 3935. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵) | ||
Theorem | nfcsbw 3934* | Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3935 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by Mario Carneiro, 12-Oct-2016.) Avoid ax-13 2374. (Revised by GG, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 | ||
Theorem | nfcsb 3935 | Bound-variable hypothesis builder for substitution into a class. Usage of this theorem is discouraged because it depends on ax-13 2374. Use the weaker nfcsbw 3934 when possible. (Contributed by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 | ||
Theorem | csbhypf 3936* | Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 3543 for class substitution version. (Contributed by NM, 19-Dec-2008.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbiebt 3937* | Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3941.) (Contributed by NM, 11-Nov-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) | ||
Theorem | csbiedf 3938* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbieb 3939* | Bidirectional conversion between an implicit class substitution hypothesis 𝑥 = 𝐴 → 𝐵 = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008.) |
⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbiebg 3940* | Bidirectional conversion between an implicit class substitution hypothesis 𝑥 = 𝐴 → 𝐵 = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 24-Mar-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) | ||
Theorem | csbiegf 3941* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ (𝐴 ∈ 𝑉 → Ⅎ𝑥𝐶) & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbief 3942* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 | ||
Theorem | csbie 3943* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019.) Reduce axiom usage. (Revised by GG, 15-Oct-2024.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 | ||
Theorem | csbieOLD 3944* | Obsolete version of csbie 3943 as of 15-Oct-2024. (Contributed by AV, 2-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 | ||
Theorem | csbied 3945* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.) Reduce axiom usage. (Revised by GG, 15-Oct-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbiedOLD 3946* | Obsolete version of csbied 3945 as of 15-Oct-2024. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbied2 3947* | Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷) | ||
Theorem | csbie2t 3948* | Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 3949). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷) | ||
Theorem | csbie2 3949* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷 | ||
Theorem | csbie2g 3950* | Conversion of implicit substitution to explicit class substitution. This version of csbie 3943 avoids a disjointness condition on 𝑥, 𝐴 and 𝑥, 𝐷 by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) & ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷) | ||
Theorem | cbvrabcsfw 3951* | Version of cbvrabcsf 3955 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by Andrew Salmon, 13-Jul-2011.) (Revised by GG, 26-Jan-2024.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓} | ||
Theorem | cbvralcsf 3952 | A more general version of cbvralf 3357 that doesn't require 𝐴 and 𝐵 to be distinct from 𝑥 or 𝑦. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvrexcsf 3953 | A more general version of cbvrexf 3358 that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by Andrew Salmon, 13-Jul-2011.) (Proof shortened by Mario Carneiro, 7-Dec-2014.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvreucsf 3954 | A more general version of cbvreuv 3427 that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvrabcsf 3955 | A more general version of cbvrab 3476 with no distinct variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓} | ||
Theorem | cbvralv2 3956* | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒) | ||
Theorem | cbvrexv2 3957* | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒) | ||
Theorem | rspc2vd 3958* | Deduction version of 2-variable restricted specialization, using implicit substitution. Notice that the class 𝐷 for the second set variable 𝑦 may depend on the first set variable 𝑥. (Contributed by AV, 29-Mar-2021.) |
⊢ (𝑥 = 𝐴 → (𝜃 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐸) & ⊢ (𝜑 → 𝐵 ∈ 𝐸) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜃 → 𝜓)) | ||
Syntax | cdif 3959 | Extend class notation to include class difference (read: "𝐴 minus 𝐵"). |
class (𝐴 ∖ 𝐵) | ||
Syntax | cun 3960 | Extend class notation to include union of two classes (read: "𝐴 union 𝐵"). |
class (𝐴 ∪ 𝐵) | ||
Syntax | cin 3961 | Extend class notation to include the intersection of two classes (read: "𝐴 intersect 𝐵"). |
class (𝐴 ∩ 𝐵) | ||
Syntax | wss 3962 | Extend wff notation to include the subclass relation. This is read "𝐴 is a subclass of 𝐵 " or "𝐵 includes 𝐴". When 𝐴 exists as a set, it is also read "𝐴 is a subset of 𝐵". |
wff 𝐴 ⊆ 𝐵 | ||
Syntax | wpss 3963 | Extend wff notation with proper subclass relation. |
wff 𝐴 ⊊ 𝐵 | ||
Theorem | difjust 3964* | Soundness justification theorem for df-dif 3965. (Contributed by Rodolfo Medina, 27-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)} | ||
Definition | df-dif 3965* | Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. For example, ({1, 3} ∖ {1, 8}) = {3} (ex-dif 30451). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3967) and intersection (𝐴 ∩ 𝐵) (df-in 3969). Several notations are used in the literature; we chose the ∖ convention used in Definition 5.3 of [Eisenberg] p. 67 instead of the more common minus sign to reserve the latter for later use in, e.g., arithmetic. We will use the terminology "𝐴 excludes 𝐵 " to mean 𝐴 ∖ 𝐵. We will use "𝐵 is removed from 𝐴 " to mean 𝐴 ∖ {𝐵} i.e. the removal of an element or equivalently the exclusion of a singleton. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} | ||
Theorem | unjust 3966* | Soundness justification theorem for df-un 3967. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)} | ||
Definition | df-un 3967* | Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∪ {1, 8}) = {1, 3, 8} (ex-un 30452). Contrast this operation with difference (𝐴 ∖ 𝐵) (df-dif 3965) and intersection (𝐴 ∩ 𝐵) (df-in 3969). For an alternate definition in terms of class difference, requiring no dummy variables, see dfun2 4275. For union defined in terms of intersection, see dfun3 4281. (Contributed by NM, 23-Aug-1993.) |
⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} | ||
Theorem | injust 3968* | Soundness justification theorem for df-in 3969. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} | ||
Definition | df-in 3969* | Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 30453). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3967) and difference (𝐴 ∖ 𝐵) (df-dif 3965). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4276 and dfin4 4283. For intersection defined in terms of union, see dfin3 4282. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | ||
Theorem | dfin5 3970* | Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.) |
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} | ||
Theorem | dfdif2 3971* | Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.) |
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵} | ||
Theorem | eldif 3972 | Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)) | ||
Theorem | eldifd 3973 | If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3972. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) | ||
Theorem | eldifad 3974 | If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3972. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐵) | ||
Theorem | eldifbd 3975 | If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3972. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | elneeldif 3976 | The elements of a set difference and the minuend are not equal. (Contributed by AV, 21-Oct-2023.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → 𝑋 ≠ 𝑌) | ||
Theorem | velcomp 3977 | Characterization of setvar elements of the complement of a class. (Contributed by Andrew Salmon, 15-Jul-2011.) |
⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴) | ||
Theorem | elin 3978 | Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | ||
Definition | df-ss 3979* |
Define the subclass relationship. Definition 5.9 of [TakeutiZaring]
p. 17. For example, {1, 2} ⊆ {1, 2, 3}
(ex-ss 30455). Note
that 𝐴 ⊆ 𝐴 (proved in ssid 4017). Contrast this relationship with
the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3982). For an
alternative definition, not requiring a dummy variable, see dfss2 3980.
Other possible definitions are given by dfss3 3983, dfss4 4274, sspss 4111,
ssequn1 4195, ssequn2 4198, sseqin2 4230, and ssdif0 4371.
We prefer the label "ss" ("subset") for ⊆, despite the fact that it applies to classes. It is much more common to refer to this as the subset relation than subclass, especially since most of the time the arguments are in fact sets (and for pragmatic reasons we don't want to need to use different operations for sets). The way set.mm is set up, many things are technically classes despite morally (and provably) being sets, like 1 (cf. df-1 11160 and 1ex 11254) or ℝ ( cf. df-r 11162 and reex 11243). This has to do with the fact that there are no "set expressions": classes are expressions but there are only set variables in set.mm (cf. https://us.metamath.org/downloads/grammar-ambiguity.txt 11243). This is why we use ⊆ both for subclass relations and for subset relations and call it "subset". (Contributed by NM, 8-Jan-2002.) Revised from the original definition dfss2 3980. (Revised by GG, 15-May-2025.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | dfss2 3980 | Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3979. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3979. (Revised by GG, 15-May-2025.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) | ||
Theorem | dfss 3981 | Variant of subclass definition dfss2 3980. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵)) | ||
Definition | df-pss 3982 | Define proper subclass (or strict subclass) relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 30456). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4112). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3979). Other possible definitions are given by dfpss2 4097 and dfpss3 4098. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | ||
Theorem | dfss3 3983* | Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | dfss6 3984* | Alternate definition of subclass relationship. (Contributed by RP, 16-Apr-2020.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | ||
Theorem | dfssf 3985 | Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 3-Jul-1994.) (Revised by Andrew Salmon, 27-Aug-2011.) Avoid ax-13 2374. (Revised by GG, 19-May-2023.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | dfss3f 3986 | Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | nfss 3987 | If 𝑥 is not free in 𝐴 and 𝐵, it is not free in 𝐴 ⊆ 𝐵. (Contributed by NM, 27-Dec-1996.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵 | ||
Theorem | ssel 3988 | Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) Avoid ax-12 2174. (Revised by SN, 27-May-2024.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | ssel2 3989 | Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵) | ||
Theorem | sseli 3990 | Membership implication from subclass relationship. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) | ||
Theorem | sselii 3991 | Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐶 ∈ 𝐴 ⇒ ⊢ 𝐶 ∈ 𝐵 | ||
Theorem | sselid 3992 | Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐵) | ||
Theorem | sseld 3993 | Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | sselda 3994 | Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵) | ||
Theorem | sseldd 3995 | Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐵) | ||
Theorem | ssneld 3996 | If a class is not in another class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (¬ 𝐶 ∈ 𝐵 → ¬ 𝐶 ∈ 𝐴)) | ||
Theorem | ssneldd 3997 | If an element is not in a class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) | ||
Theorem | ssriv 3998* | Inference based on subclass definition. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
Theorem | ssrd 3999 | Deduction based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | ssrdv 4000* | Deduction based on subclass definition. (Contributed by NM, 15-Nov-1995.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |