Home | Metamath
Proof Explorer Theorem List (p. 36 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | csb2 3501* | 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 3502 | Analogue of dfsbcq 3404 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) | ||
Theorem | csbeq2 3503 | Substituting into equivalent classes gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.) |
⊢ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | cbvcsb 3504 | Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on 𝐴. (Contributed by Jeff Hankins, 13-Sep-2009.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑦⦌𝐷 | ||
Theorem | cbvcsbv 3505* | 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 | csbeq1d 3506 | Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) | ||
Theorem | csbid 3507 | Analogue of sbid 2100 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 | ||
Theorem | csbeq1a 3508 | Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵) | ||
Theorem | csbco 3509* | Composition law for chained substitutions into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ ⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | csbtt 3510 | Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐵) → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | csbconstgf 3511 | Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). (Contributed by NM, 10-Nov-2005.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | csbconstg 3512* | Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3511 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) | ||
Theorem | nfcsb1d 3513 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵) | ||
Theorem | nfcsb1 3514 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | nfcsb1v 3515* | Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | nfcsbd 3516 | Deduction version of nfcsb 3517. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵) | ||
Theorem | nfcsb 3517 | Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵 | ||
Theorem | csbhypf 3518* | Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 3226 for class substitution version. (Contributed by NM, 19-Dec-2008.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbiebt 3519* | Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3523.) (Contributed by NM, 11-Nov-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) | ||
Theorem | csbiedf 3520* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbieb 3521* | Bidirectional conversion between an implicit class substitution hypothesis 𝑥 = 𝐴 → 𝐵 = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008.) |
⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) | ||
Theorem | csbiebg 3522* | 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 3523* | 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 3524* | 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 3525* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 | ||
Theorem | csbied 3526* | 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 3527* | Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷) | ||
Theorem | csbie2t 3528* | Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 3529). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷) | ||
Theorem | csbie2 3529* | Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = 𝐷 | ||
Theorem | csbie2g 3530* | Conversion of implicit substitution to explicit class substitution. This version of csbie 3525 avoids a disjointness condition on 𝑥, 𝐴 and 𝑥, 𝐷 by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) & ⊢ (𝑦 = 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷) | ||
Theorem | cbvralcsf 3531 | A more general version of cbvralf 3141 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 3532 | A more general version of cbvrexf 3142 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 3533 | A more general version of cbvreuv 3149 that has no distinct variable restrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvrabcsf 3534 | A more general version of cbvrab 3171 with no distinct variable restrictions. (Contributed by Andrew Salmon, 13-Jul-2011.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓} | ||
Theorem | cbvralv2 3535* | 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 3536* | 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.) |
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒) | ||
Syntax | cdif 3537 | Extend class notation to include class difference (read: "𝐴 minus 𝐵"). |
class (𝐴 ∖ 𝐵) | ||
Syntax | cun 3538 | Extend class notation to include union of two classes (read: "𝐴 union 𝐵"). |
class (𝐴 ∪ 𝐵) | ||
Syntax | cin 3539 | Extend class notation to include the intersection of two classes (read: "𝐴 intersect 𝐵"). |
class (𝐴 ∩ 𝐵) | ||
Syntax | wss 3540 | 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 3541 | Extend wff notation with proper subclass relation. |
wff 𝐴 ⊊ 𝐵 | ||
Theorem | difjust 3542* | Soundness justification theorem for df-dif 3543. (Contributed by Rodolfo Medina, 27-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)} | ||
Definition | df-dif 3543* | Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. For example, ({1, 3} ∖ {1, 8}) = {3} (ex-dif 26672). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3545) and intersection (𝐴 ∩ 𝐵) (df-in 3547). 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 3544* | Soundness justification theorem for df-un 3545. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)} | ||
Definition | df-un 3545* | Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∪ {1, 8}) = {1, 3, 8} (ex-un 26673). Contrast this operation with difference (𝐴 ∖ 𝐵) (df-dif 3543) and intersection (𝐴 ∩ 𝐵) (df-in 3547). For an alternate definition in terms of class difference, requiring no dummy variables, see dfun2 3821. For union defined in terms of intersection, see dfun3 3824. (Contributed by NM, 23-Aug-1993.) |
⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)} | ||
Theorem | injust 3546* | Soundness justification theorem for df-in 3547. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} | ||
Definition | df-in 3547* | Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 26674). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3545) and difference (𝐴 ∖ 𝐵) (df-dif 3543). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 3822 and dfin4 3826. For intersection defined in terms of union, see dfin3 3825. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | ||
Theorem | dfin5 3548* | Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.) |
⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} | ||
Theorem | dfdif2 3549* | Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.) |
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐵} | ||
Theorem | eldif 3550 | Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)) | ||
Theorem | eldifd 3551 | If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3550. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) | ||
Theorem | eldifad 3552 | If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3550. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐵) | ||
Theorem | eldifbd 3553 | If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3550. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) | ||
Definition | df-ss 3554 | Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 26676). Note that 𝐴 ⊆ 𝐴 (proved in ssid 3587). Contrast this relationship with the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 3556). For a more traditional definition, but requiring a dummy variable, see dfss2 3557. Other possible definitions are given by dfss3 3558, dfss4 3820, sspss 3668, ssequn1 3745, ssequn2 3748, sseqin2 3779, and ssdif0 3896. (Contributed by NM, 27-Apr-1994.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) | ||
Theorem | dfss 3555 | Variant of subclass definition df-ss 3554. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵)) | ||
Definition | df-pss 3556 | Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 26677). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 3669). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3554). Other possible definitions are given by dfpss2 3654 and dfpss3 3655. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | ||
Theorem | dfss2 3557* | Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | dfss3 3558* | Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | dfss2f 3559 | 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.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | dfss3f 3560 | Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | nfss 3561 | If 𝑥 is not free in 𝐴 and 𝐵, it is not free in 𝐴 ⊆ 𝐵. (Contributed by NM, 27-Dec-1996.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵 | ||
Theorem | ssel 3562 | Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | ssel2 3563 | Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵) | ||
Theorem | sseli 3564 | Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵) | ||
Theorem | sselii 3565 | Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐶 ∈ 𝐴 ⇒ ⊢ 𝐶 ∈ 𝐵 | ||
Theorem | sseldi 3566 | Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐵) | ||
Theorem | sseld 3567 | Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) | ||
Theorem | sselda 3568 | Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵) | ||
Theorem | sseldd 3569 | Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐵) | ||
Theorem | ssneld 3570 | 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 3571 | 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 3572* | Inference rule based on subclass definition. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
Theorem | ssrd 3573 | Deduction rule based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | ssrdv 3574* | Deduction rule based on subclass definition. (Contributed by NM, 15-Nov-1995.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | sstr2 3575 | Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) | ||
Theorem | sstr 3576 | Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | ||
Theorem | sstri 3577 | Subclass transitivity inference. (Contributed by NM, 5-May-2000.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | sstrd 3578 | Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | syl5ss 3579 | Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | syl6ss 3580 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sylan9ss 3581 | A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜓 → 𝐵 ⊆ 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶) | ||
Theorem | sylan9ssr 3582 | A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜓 → 𝐵 ⊆ 𝐶) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝐴 ⊆ 𝐶) | ||
Theorem | eqss 3583 | The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 21-May-1993.) |
⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | ||
Theorem | eqssi 3584 | Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐵 ⊆ 𝐴 ⇒ ⊢ 𝐴 = 𝐵 | ||
Theorem | eqssd 3585 | Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | eqrd 3586 | Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | ssid 3587 | 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 | ssv 3588 | Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.) |
⊢ 𝐴 ⊆ V | ||
Theorem | sseq1 3589 | Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | ||
Theorem | sseq2 3590 | Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.) |
⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | ||
Theorem | sseq12 3591 | Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)) | ||
Theorem | sseq1i 3592 | An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) | ||
Theorem | sseq2i 3593 | An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) | ||
Theorem | sseq12i 3594 | An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷) | ||
Theorem | sseq1d 3595 | An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | ||
Theorem | sseq2d 3596 | An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | ||
Theorem | sseq12d 3597 | An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)) | ||
Theorem | eqsstri 3598 | Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | eqsstr3i 3599 | Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.) |
⊢ 𝐵 = 𝐴 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | sseqtri 3600 | Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |