Home | Metamath
Proof Explorer Theorem List (p. 40 of 449) | < 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: | Metamath Proof Explorer
(1-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | csbconstgi 3901* | 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 3902 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) | ||
Theorem | nfcsb1 3903 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | nfcsb1v 3904* | Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | nfcsbd 3905 | Deduction version of nfcsb 3907. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵) | ||
Theorem | nfcsbw 3906* | Version of nfcsb 3907 with a disjoint variable condition, which does not require ax-13 2381. (Contributed by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 | ||
Theorem | nfcsb 3907 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 | ||
Theorem | csbhypf 3908* | Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 3550 for class substitution version. (Contributed by NM, 19-Dec-2008.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbiebt 3909* | Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3913.) (Contributed by NM, 11-Nov-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) | ||
Theorem | csbiedf 3910* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbieb 3911* | Bidirectional conversion between an implicit class substitution hypothesis 𝑥 = 𝐴 → 𝐵 = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008.) |
⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbiebg 3912* | 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 3913* | 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 3914* | 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 3915* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 | ||
Theorem | csbied 3916* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbied2 3917* | Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷) | ||
Theorem | csbie2t 3918* | Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 3919). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷) | ||
Theorem | csbie2 3919* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷 | ||
Theorem | csbie2g 3920* | Conversion of implicit substitution to explicit class substitution. This version of csbie 3915 avoids a disjointness condition on 𝑥, 𝐴 and 𝑥, 𝐷 by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) & ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷) | ||
Theorem | cbvrabcsfw 3921* | Version of cbvrabcsf 3925 with a disjoint variable condition, which does not require ax-13 2381. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓} | ||
Theorem | cbvralcsf 3922 | A more general version of cbvralf 3437 that doesn't require 𝐴 and 𝐵 to be distinct from 𝑥 or 𝑦. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvrexcsf 3923 | A more general version of cbvrexf 3438 that has no distinct variable restrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.) (Proof shortened by Mario Carneiro, 7-Dec-2014.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvreucsf 3924 | A more general version of cbvreuv 3452 that has no distinct variable restrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvrabcsf 3925 | A more general version of cbvrab 3488 with no distinct variable restrictions. (Contributed by Andrew Salmon, 13-Jul-2011.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓} | ||
Theorem | cbvralv2 3926* | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒) | ||
Theorem | cbvrexv2 3927* | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒) | ||
Theorem | vtocl2dOLD 3928* | Obsolete version of vtocl2d 3555 as of 19-Oct-2023. (Contributed by Thierry Arnoux, 25-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | rspc2vd 3929* | 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 3930 | Extend class notation to include class difference (read: "𝐴 minus 𝐵"). |
class (𝐴 ∖ 𝐵) | ||
Syntax | cun 3931 | Extend class notation to include union of two classes (read: "𝐴 union 𝐵"). |
class (𝐴 ∪ 𝐵) | ||
Syntax | cin 3932 | Extend class notation to include the intersection of two classes (read: "𝐴 intersect 𝐵"). |
class (𝐴 ∩ 𝐵) | ||
Syntax | wss 3933 | 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 3934 | Extend wff notation with proper subclass relation. |
wff 𝐴 ⊊ 𝐵 | ||
Theorem | difjust 3935* | Soundness justification theorem for df-dif 3936. (Contributed by Rodolfo Medina, 27-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)} | ||
Definition | df-dif 3936* | Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. For example, ({1, 3} ∖ {1, 8}) = {3} (ex-dif 28129). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3938) and intersection (𝐴 ∩ 𝐵) (df-in 3940). 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 3937* | Soundness justification theorem for df-un 3938. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)} | ||
Definition | df-un 3938* | Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∪ {1, 8}) = {1, 3, 8} (ex-un 28130). Contrast this operation with difference (𝐴 ∖ 𝐵) (df-dif 3936) and intersection (𝐴 ∩ 𝐵) (df-in 3940). For an alternate definition in terms of class difference, requiring no dummy variables, see dfun2 4233. For union defined in terms of intersection, see dfun3 4239. (Contributed by NM, 23-Aug-1993.) |
⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} | ||
Theorem | injust 3939* | Soundness justification theorem for df-in 3940. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} | ||
Definition | df-in 3940* | Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 28131). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3938) and difference (𝐴 ∖ 𝐵) (df-dif 3936). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4234 and dfin4 4241. For intersection defined in terms of union, see dfin3 4240. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | ||
Theorem | dfin5 3941* | Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.) |
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} | ||
Theorem | dfdif2 3942* | Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.) |
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵} | ||
Theorem | eldif 3943 | Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)) | ||
Theorem | eldifd 3944 | If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3943. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) | ||
Theorem | eldifad 3945 | If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3943. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐵) | ||
Theorem | eldifbd 3946 | If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3943. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | elneeldif 3947 | The elements of a set difference and the minuend are not equal. (Contributed by AV, 21-Oct-2023.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → 𝑋 ≠ 𝑌) | ||
Theorem | velcomp 3948 | Characterization of setvar elements of the complement of a class. (Contributed by Andrew Salmon, 15-Jul-2011.) |
⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴) | ||
Definition | df-ss 3949 |
Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18.
For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 28133). Note that
𝐴
⊆ 𝐴 (proved in
ssid 3986). Contrast this relationship with the
relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3951). For a more
traditional definition, but requiring a dummy variable, see dfss2 3952.
Other possible definitions are given by dfss3 3953, dfss4 4232, sspss 4073,
ssequn1 4153, ssequn2 4156, sseqin2 4189, and ssdif0 4320.
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 10533 and 1ex 10625) or ℝ ( cf. df-r 10535 and reex 10616). 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 10616). This is why we use ⊆ both for subclass relations and for subset relations and call it "subset". (Contributed by NM, 27-Apr-1994.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) | ||
Theorem | dfss 3950 | Variant of subclass definition df-ss 3949. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵)) | ||
Definition | df-pss 3951 | 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 28134). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4074). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3949). Other possible definitions are given by dfpss2 4059 and dfpss3 4060. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | ||
Theorem | dfss2 3952* | Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | dfss3 3953* | Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | dfss6 3954* | Alternate definition of subclass relationship. (Contributed by RP, 16-Apr-2020.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | ||
Theorem | dfss2f 3955 | 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 2381. (Revised by Gino Giotto, 19-May-2023.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | dfss3f 3956 | Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | nfss 3957 | If 𝑥 is not free in 𝐴 and 𝐵, it is not free in 𝐴 ⊆ 𝐵. (Contributed by NM, 27-Dec-1996.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵 | ||
Theorem | ssel 3958 | Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | ssel2 3959 | Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵) | ||
Theorem | sseli 3960 | Membership implication from subclass relationship. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) | ||
Theorem | sselii 3961 | Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐶 ∈ 𝐴 ⇒ ⊢ 𝐶 ∈ 𝐵 | ||
Theorem | sseldi 3962 | Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐵) | ||
Theorem | sseld 3963 | Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | sselda 3964 | Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵) | ||
Theorem | sseldd 3965 | Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐵) | ||
Theorem | ssneld 3966 | 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 3967 | 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 3968* | Inference based on subclass definition. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
Theorem | ssrd 3969 | Deduction based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | ssrdv 3970* | Deduction based on subclass definition. (Contributed by NM, 15-Nov-1995.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | sstr2 3971 | Transitivity of subclass relationship. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) | ||
Theorem | sstr 3972 | Transitivity of subclass relationship. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | ||
Theorem | sstri 3973 | Subclass transitivity inference. (Contributed by NM, 5-May-2000.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | sstrd 3974 | Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sstrid 3975 | Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sstrdi 3976 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sylan9ss 3977 | A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜓 → 𝐵 ⊆ 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶) | ||
Theorem | sylan9ssr 3978 | A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜓 → 𝐵 ⊆ 𝐶) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝐴 ⊆ 𝐶) | ||
Theorem | eqss 3979 | The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 21-May-1993.) |
⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | ||
Theorem | eqssi 3980 | Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐵 ⊆ 𝐴 ⇒ ⊢ 𝐴 = 𝐵 | ||
Theorem | eqssd 3981 | Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | sssseq 3982 | 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 3983 | Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017.) (Proof shortened by BJ, 1-Dec-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | eqri 3984 | Infer equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 7-Oct-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ⇒ ⊢ 𝐴 = 𝐵 | ||
Theorem | eqelssd 3985* | Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | ssid 3986 | 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 3987 | Weakening of ssid 3986. (Contributed by BJ, 1-Sep-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐴) | ||
Theorem | ssv 3988 | Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.) |
⊢ 𝐴 ⊆ V | ||
Theorem | sseq1 3989 | Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | ||
Theorem | sseq2 3990 | Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.) |
⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | ||
Theorem | sseq12 3991 | Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)) | ||
Theorem | sseq1i 3992 | An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) | ||
Theorem | sseq2i 3993 | An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) | ||
Theorem | sseq12i 3994 | An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷) | ||
Theorem | sseq1d 3995 | An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | ||
Theorem | sseq2d 3996 | An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | ||
Theorem | sseq12d 3997 | An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)) | ||
Theorem | eqsstri 3998 | Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | eqsstrri 3999 | Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.) |
⊢ 𝐵 = 𝐴 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | sseqtri 4000 | Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |