![]() |
Metamath
Proof Explorer Theorem List (p. 40 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | csbcow 3901* | Composition law for chained substitutions into a class. Version of csbco 3902 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by NM, 10-Nov-2005.) Avoid ax-13 2365. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | csbco 3902* | Composition law for chained substitutions into a class. Usage of this theorem is discouraged because it depends on ax-13 2365. Use the weaker csbcow 3901 when possible. (Contributed by NM, 10-Nov-2005.) (New usage is discouraged.) |
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | csbtt 3903 | Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐵) → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | csbconstgf 3904 | Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by NM, 10-Nov-2005.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | csbconstg 3905* | Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3904 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) Avoid ax-12 2166. (Revised by Gino Giotto, 15-Oct-2024.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | csbconstgOLD 3906* | Obsolete version of csbconstg 3905 as of 15-Oct-2024. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | csbgfi 3907 | 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 3908* | 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 3909 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) | ||
Theorem | nfcsb1 3910 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | nfcsb1v 3911* | Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | nfcsbd 3912 | Deduction version of nfcsb 3914. Usage of this theorem is discouraged because it depends on ax-13 2365. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵) | ||
Theorem | nfcsbw 3913* | Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3914 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by Mario Carneiro, 12-Oct-2016.) Avoid ax-13 2365. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 | ||
Theorem | nfcsb 3914 | Bound-variable hypothesis builder for substitution into a class. Usage of this theorem is discouraged because it depends on ax-13 2365. Use the weaker nfcsbw 3913 when possible. (Contributed by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 | ||
Theorem | csbhypf 3915* | Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 3529 for class substitution version. (Contributed by NM, 19-Dec-2008.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbiebt 3916* | Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3920.) (Contributed by NM, 11-Nov-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) | ||
Theorem | csbiedf 3917* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbieb 3918* | Bidirectional conversion between an implicit class substitution hypothesis 𝑥 = 𝐴 → 𝐵 = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008.) |
⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbiebg 3919* | 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 3920* | 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 3921* | 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 3922* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019.) Reduce axiom usage. (Revised by Gino Giotto, 15-Oct-2024.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 | ||
Theorem | csbieOLD 3923* | Obsolete version of csbie 3922 as of 15-Oct-2024. (Contributed by AV, 2-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 | ||
Theorem | csbied 3924* | 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 Gino Giotto, 15-Oct-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbiedOLD 3925* | Obsolete version of csbied 3924 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 3926* | Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷) | ||
Theorem | csbie2t 3927* | Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 3928). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷) | ||
Theorem | csbie2 3928* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷 | ||
Theorem | csbie2g 3929* | Conversion of implicit substitution to explicit class substitution. This version of csbie 3922 avoids a disjointness condition on 𝑥, 𝐴 and 𝑥, 𝐷 by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) & ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷) | ||
Theorem | cbvrabcsfw 3930* | Version of cbvrabcsf 3934 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by Andrew Salmon, 13-Jul-2011.) (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓} | ||
Theorem | cbvralcsf 3931 | A more general version of cbvralf 3344 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 2365. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvrexcsf 3932 | A more general version of cbvrexf 3345 that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2365. (Contributed by Andrew Salmon, 13-Jul-2011.) (Proof shortened by Mario Carneiro, 7-Dec-2014.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvreucsf 3933 | A more general version of cbvreuv 3414 that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2365. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvrabcsf 3934 | A more general version of cbvrab 3462 with no distinct variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2365. (Contributed by Andrew Salmon, 13-Jul-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓} | ||
Theorem | cbvralv2 3935* | 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 2365. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒) | ||
Theorem | cbvrexv2 3936* | 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 2365. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒) | ||
Theorem | rspc2vd 3937* | 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 3938 | Extend class notation to include class difference (read: "𝐴 minus 𝐵"). |
class (𝐴 ∖ 𝐵) | ||
Syntax | cun 3939 | Extend class notation to include union of two classes (read: "𝐴 union 𝐵"). |
class (𝐴 ∪ 𝐵) | ||
Syntax | cin 3940 | Extend class notation to include the intersection of two classes (read: "𝐴 intersect 𝐵"). |
class (𝐴 ∩ 𝐵) | ||
Syntax | wss 3941 | 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 3942 | Extend wff notation with proper subclass relation. |
wff 𝐴 ⊊ 𝐵 | ||
Theorem | difjust 3943* | Soundness justification theorem for df-dif 3944. (Contributed by Rodolfo Medina, 27-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)} | ||
Definition | df-dif 3944* | Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. For example, ({1, 3} ∖ {1, 8}) = {3} (ex-dif 30272). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3946) and intersection (𝐴 ∩ 𝐵) (df-in 3948). 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 3945* | Soundness justification theorem for df-un 3946. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)} | ||
Definition | df-un 3946* | Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∪ {1, 8}) = {1, 3, 8} (ex-un 30273). Contrast this operation with difference (𝐴 ∖ 𝐵) (df-dif 3944) and intersection (𝐴 ∩ 𝐵) (df-in 3948). For an alternate definition in terms of class difference, requiring no dummy variables, see dfun2 4255. For union defined in terms of intersection, see dfun3 4261. (Contributed by NM, 23-Aug-1993.) |
⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} | ||
Theorem | injust 3947* | Soundness justification theorem for df-in 3948. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} | ||
Definition | df-in 3948* | Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 30274). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3946) and difference (𝐴 ∖ 𝐵) (df-dif 3944). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4256 and dfin4 4263. For intersection defined in terms of union, see dfin3 4262. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | ||
Theorem | dfin5 3949* | Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.) |
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} | ||
Theorem | dfdif2 3950* | Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.) |
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵} | ||
Theorem | eldif 3951 | Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)) | ||
Theorem | eldifd 3952 | If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3951. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) | ||
Theorem | eldifad 3953 | If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3951. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐵) | ||
Theorem | eldifbd 3954 | If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3951. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | elneeldif 3955 | The elements of a set difference and the minuend are not equal. (Contributed by AV, 21-Oct-2023.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → 𝑋 ≠ 𝑌) | ||
Theorem | velcomp 3956 | Characterization of setvar elements of the complement of a class. (Contributed by Andrew Salmon, 15-Jul-2011.) |
⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴) | ||
Theorem | elin 3957 | Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | ||
Definition | df-ss 3958* |
Define the subclass relationship. Definition 5.9 of [TakeutiZaring]
p. 17. For example, {1, 2} ⊆ {1, 2, 3}
(ex-ss 30276). Note
that 𝐴 ⊆ 𝐴 (proved in ssid 3996). Contrast this relationship with
the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3961). For an
alternative definition, not requiring a dummy variable, see dfss2 3959.
Other possible definitions are given by dfss3 3962, dfss4 4254, sspss 4092,
ssequn1 4175, ssequn2 4178, sseqin2 4210, and ssdif0 4360.
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 11141 and 1ex 11235) or ℝ ( cf. df-r 11143 and reex 11224). 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 11224). 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 3959. (Revised by GG, 15-May-2025.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | dfss2 3959 | Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This was the original definition before df-ss 3958. (Contributed by NM, 27-Apr-1994.) Revise df-ss 3958. (Revised by GG, 15-May-2025.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) | ||
Theorem | dfss 3960 | Variant of subclass definition dfss2 3959. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵)) | ||
Definition | df-pss 3961 | 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 30277). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4093). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3958). Other possible definitions are given by dfpss2 4078 and dfpss3 4079. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | ||
Theorem | dfss3 3962* | Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | dfss6 3963* | Alternate definition of subclass relationship. (Contributed by RP, 16-Apr-2020.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | ||
Theorem | dfssf 3964 | 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 2365. (Revised by Gino Giotto, 19-May-2023.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | dfss3f 3965 | Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | nfss 3966 | If 𝑥 is not free in 𝐴 and 𝐵, it is not free in 𝐴 ⊆ 𝐵. (Contributed by NM, 27-Dec-1996.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵 | ||
Theorem | ssel 3967 | Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) Avoid ax-12 2166. (Revised by SN, 27-May-2024.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | ssel2 3968 | Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵) | ||
Theorem | sseli 3969 | Membership implication from subclass relationship. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) | ||
Theorem | sselii 3970 | Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐶 ∈ 𝐴 ⇒ ⊢ 𝐶 ∈ 𝐵 | ||
Theorem | sselid 3971 | Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐵) | ||
Theorem | sseld 3972 | Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | sselda 3973 | Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵) | ||
Theorem | sseldd 3974 | Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐵) | ||
Theorem | ssneld 3975 | 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 3976 | 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 3977* | Inference based on subclass definition. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
Theorem | ssrd 3978 | Deduction based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | ssrdv 3979* | Deduction based on subclass definition. (Contributed by NM, 15-Nov-1995.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | sstr2 3980 | Transitivity of subclass relationship. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) Avoid axioms. (Revised by GG, 19-May-2025.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) | ||
Theorem | sstr2OLD 3981 | Obsolete version of sstr2 3980 as of 19-May-2025. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) | ||
Theorem | sstr 3982 | Transitivity of subclass relationship. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | ||
Theorem | sstri 3983 | Subclass transitivity inference. (Contributed by NM, 5-May-2000.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | sstrd 3984 | Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sstrid 3985 | Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sstrdi 3986 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sylan9ss 3987 | A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜓 → 𝐵 ⊆ 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶) | ||
Theorem | sylan9ssr 3988 | A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜓 → 𝐵 ⊆ 𝐶) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝐴 ⊆ 𝐶) | ||
Theorem | eqss 3989 | The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 21-May-1993.) |
⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | ||
Theorem | eqssi 3990 | Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐵 ⊆ 𝐴 ⇒ ⊢ 𝐴 = 𝐵 | ||
Theorem | eqssd 3991 | Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | sssseq 3992 | If a class is a subclass of another class, then the classes are equal if and only if the other class is a subclass of the first class. (Contributed by AV, 23-Dec-2020.) |
⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | eqrd 3993 | Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017.) (Proof shortened by BJ, 1-Dec-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | eqri 3994 | Infer equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 7-Oct-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ⇒ ⊢ 𝐴 = 𝐵 | ||
Theorem | eqelssd 3995* | Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | ssid 3996 | Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ 𝐴 ⊆ 𝐴 | ||
Theorem | ssidd 3997 | Weakening of ssid 3996. (Contributed by BJ, 1-Sep-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐴) | ||
Theorem | ssv 3998 | Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.) |
⊢ 𝐴 ⊆ V | ||
Theorem | sseq1 3999 | Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | ||
Theorem | sseq2 4000 | Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.) |
⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |