Home | Metamath
Proof Explorer Theorem List (p. 41 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 | sseqtrri 4001 | Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | eqsstrd 4002 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | eqsstrrd 4003 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sseqtrd 4004 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sseqtrrd 4005 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | 3sstr3i 4006 | Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ 𝐶 ⊆ 𝐷 | ||
Theorem | 3sstr4i 4007 | Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ 𝐶 ⊆ 𝐷 | ||
Theorem | 3sstr3g 4008 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ⊆ 𝐷) | ||
Theorem | 3sstr4g 4009 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 ⊆ 𝐷) | ||
Theorem | 3sstr3d 4010 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶 ⊆ 𝐷) | ||
Theorem | 3sstr4d 4011 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 30-Nov-1995.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐴) & ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ⊆ 𝐷) | ||
Theorem | eqsstrid 4012 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | eqsstrrid 4013 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sseqtrdi 4014 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sseqtrrdi 4015 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sseqtrid 4016 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐵 ⊆ 𝐴 & ⊢ (𝜑 → 𝐴 = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | ||
Theorem | sseqtrrid 4017 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐵 ⊆ 𝐴 & ⊢ (𝜑 → 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | ||
Theorem | eqsstrdi 4018 | A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | eqsstrrdi 4019 | A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | eqimss 4020 | Equality implies the subclass relation. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | ||
Theorem | eqimss2 4021 | Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.) |
⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵) | ||
Theorem | eqimssi 4022 | Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
Theorem | eqimss2i 4023 | Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝐵 ⊆ 𝐴 | ||
Theorem | nssne1 4024 | Two classes are different if they don't include the same class. (Contributed by NM, 23-Apr-2015.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ⊆ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | nssne2 4025 | Two classes are different if they are not subclasses of the same class. (Contributed by NM, 23-Apr-2015.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ ¬ 𝐵 ⊆ 𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | nss 4026* | Negation of subclass relationship. Exercise 13 of [TakeutiZaring] p. 18. (Contributed by NM, 25-Feb-1996.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | ||
Theorem | nelss 4027 | Demonstrate by witnesses that two classes lack a subclass relation. (Contributed by Stefan O'Rear, 5-Feb-2015.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 ⊆ 𝐶) | ||
Theorem | ssrexf 4028 | Restricted existential quantification follows from a subclass relationship. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ssrmof 4029 | "At most one" existential quantification restricted to a subclass. (Contributed by Thierry Arnoux, 8-Oct-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 → (∃*𝑥 ∈ 𝐵 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | ssralv 4030* | Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.) |
⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | ssrexv 4031* | Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.) |
⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ss2ralv 4032* | Two quantifications restricted to a subclass. (Contributed by AV, 11-Mar-2023.) |
⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑)) | ||
Theorem | ss2rexv 4033* | Two existential quantifications restricted to a subclass. (Contributed by AV, 11-Mar-2023.) |
⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝜑)) | ||
Theorem | ralss 4034* | Restricted universal quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑))) | ||
Theorem | rexss 4035* | Restricted existential quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
Theorem | ss2ab 4036 | Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994.) |
⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | abss 4037* | Class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.) |
⊢ ({𝑥 ∣ 𝜑} ⊆ 𝐴 ↔ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴)) | ||
Theorem | ssab 4038* | Subclass of a class abstraction. (Contributed by NM, 16-Aug-2006.) |
⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | ssabral 4039* | The relation for a subclass of a class abstraction is equivalent to restricted quantification. (Contributed by NM, 6-Sep-2006.) |
⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ss2abi 4040 | Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} | ||
Theorem | ss2abdv 4041* | Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒}) | ||
Theorem | abssdv 4042* | Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) |
⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴) | ||
Theorem | abssi 4043* | Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) |
⊢ (𝜑 → 𝑥 ∈ 𝐴) ⇒ ⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴 | ||
Theorem | ss2rab 4044 | Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) | ||
Theorem | rabss 4045* | Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵)) | ||
Theorem | ssrab 4046* | Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.) |
⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ssrabdv 4047* | Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 31-Aug-2006.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
Theorem | rabssdv 4048* | Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 2-Feb-2015.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵) | ||
Theorem | ss2rabdv 4049* | Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | ss2rabi 4050 | Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabss2 4051* | Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | ssab2 4052* | Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 | ||
Theorem | ssrab2 4053* | Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 | ||
Theorem | ssrab3 4054* | Subclass relation for a restricted class abstraction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} ⇒ ⊢ 𝐵 ⊆ 𝐴 | ||
Theorem | rabssrabd 4055* | Subclass of a restricted class abstraction. (Contributed by AV, 4-Jun-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝑥 ∈ 𝐴) → 𝜒) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | ssrabeq 4056* | If the restricting class of a restricted class abstraction is a subset of this restricted class abstraction, it is equal to this restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |
⊢ (𝑉 ⊆ {𝑥 ∈ 𝑉 ∣ 𝜑} ↔ 𝑉 = {𝑥 ∈ 𝑉 ∣ 𝜑}) | ||
Theorem | rabssab 4057 | A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} | ||
Theorem | uniiunlem 4058* | A subset relationship useful for converting union to indexed union using dfiun2 4949 or dfiun2g 4946 and intersection to indexed intersection using dfiin2 4950. (Contributed by NM, 5-Oct-2006.) (Proof shortened by Mario Carneiro, 26-Sep-2015.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 → (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐶)) | ||
Theorem | dfpss2 4059 | Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | ||
Theorem | dfpss3 4060 | Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴)) | ||
Theorem | psseq1 4061 | Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) | ||
Theorem | psseq2 4062 | Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)) | ||
Theorem | psseq1i 4063 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶) | ||
Theorem | psseq2i 4064 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵) | ||
Theorem | psseq12i 4065 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷) | ||
Theorem | psseq1d 4066 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) | ||
Theorem | psseq2d 4067 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)) | ||
Theorem | psseq12d 4068 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷)) | ||
Theorem | pssss 4069 | A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | ||
Theorem | pssne 4070 | Two classes in a proper subclass relationship are not equal. (Contributed by NM, 16-Feb-2015.) |
⊢ (𝐴 ⊊ 𝐵 → 𝐴 ≠ 𝐵) | ||
Theorem | pssssd 4071 | Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.) |
⊢ (𝜑 → 𝐴 ⊊ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | pssned 4072 | Proper subclasses are unequal. Deduction form of pssne 4070. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊊ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | sspss 4073 | Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | pssirr 4074 | Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) |
⊢ ¬ 𝐴 ⊊ 𝐴 | ||
Theorem | pssn2lp 4075 | Proper subclass has no 2-cycle loops. Compare Theorem 8 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ¬ (𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐴) | ||
Theorem | sspsstri 4076 | Two ways of stating trichotomy with respect to inclusion. (Contributed by NM, 12-Aug-2004.) |
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴)) | ||
Theorem | ssnpss 4077 | Partial trichotomy law for subclasses. (Contributed by NM, 16-May-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → ¬ 𝐵 ⊊ 𝐴) | ||
Theorem | psstr 4078 | Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) |
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶) | ||
Theorem | sspsstr 4079 | Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶) | ||
Theorem | psssstr 4080 | Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.) |
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊊ 𝐶) | ||
Theorem | psstrd 4081 | Proper subclass inclusion is transitive. Deduction form of psstr 4078. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊊ 𝐵) & ⊢ (𝜑 → 𝐵 ⊊ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐶) | ||
Theorem | sspsstrd 4082 | Transitivity involving subclass and proper subclass inclusion. Deduction form of sspsstr 4079. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊊ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐶) | ||
Theorem | psssstrd 4083 | Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 4080. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊊ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐶) | ||
Theorem | npss 4084 | A class is not a proper subclass of another iff it satisfies a one-directional form of eqss 3979. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (¬ 𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 → 𝐴 = 𝐵)) | ||
Theorem | ssnelpss 4085 | A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002.) |
⊢ (𝐴 ⊆ 𝐵 → ((𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴) → 𝐴 ⊊ 𝐵)) | ||
Theorem | ssnelpssd 4086 | Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 4085. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐵) | ||
Theorem | ssexnelpss 4087* | If there is an element of a class which is not contained in a subclass, the subclass is a proper subclass. (Contributed by AV, 29-Jan-2020.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝑥 ∉ 𝐴) → 𝐴 ⊊ 𝐵) | ||
Theorem | dfdif3 4088* | Alternate definition of class difference. (Contributed by BJ and Jim Kingdon, 16-Jun-2022.) |
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦} | ||
Theorem | difeq1 4089 | Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) | ||
Theorem | difeq2 4090 | Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) | ||
Theorem | difeq12 4091 | Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)) | ||
Theorem | difeq1i 4092 | Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶) | ||
Theorem | difeq2i 4093 | Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵) | ||
Theorem | difeq12i 4094 | Equality inference for class difference. (Contributed by NM, 29-Aug-2004.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷) | ||
Theorem | difeq1d 4095 | Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) | ||
Theorem | difeq2d 4096 | Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) | ||
Theorem | difeq12d 4097 | Equality deduction for class difference. (Contributed by FL, 29-May-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)) | ||
Theorem | difeqri 4098* | Inference from membership to difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ⇒ ⊢ (𝐴 ∖ 𝐵) = 𝐶 | ||
Theorem | nfdif 4099 | Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵) | ||
Theorem | eldifi 4100 | Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |