Home | Metamath
Proof Explorer Theorem List (p. 37 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 | sseqtr4i 3601 | Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
Theorem | eqsstrd 3602 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | eqsstr3d 3603 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sseqtrd 3604 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | sseqtr4d 3605 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | 3sstr3i 3606 | 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 3607 | 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 3608 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ⊆ 𝐷) | ||
Theorem | 3sstr4g 3609 | 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 3610 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶 ⊆ 𝐷) | ||
Theorem | 3sstr4d 3611 | 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 | syl5eqss 3612 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | syl5eqssr 3613 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | syl6sseq 3614 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | syl6sseqr 3615 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | syl5sseq 3616 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐵 ⊆ 𝐴 & ⊢ (𝜑 → 𝐴 = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | ||
Theorem | syl5sseqr 3617 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐵 ⊆ 𝐴 & ⊢ (𝜑 → 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | ||
Theorem | syl6eqss 3618 | A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | syl6eqssr 3619 | A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | eqimss 3620 | Equality implies the subclass relation. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | ||
Theorem | eqimss2 3621 | Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.) |
⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵) | ||
Theorem | eqimssi 3622 | Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
Theorem | eqimss2i 3623 | Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝐵 ⊆ 𝐴 | ||
Theorem | nssne1 3624 | Two classes are different if they don't include the same class. (Contributed by NM, 23-Apr-2015.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ⊆ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | nssne2 3625 | Two classes are different if they are not subclasses of the same class. (Contributed by NM, 23-Apr-2015.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ ¬ 𝐵 ⊆ 𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | nss 3626* | 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 3627 | Demonstrate by witnesses that two classes lack a subclass relation. (Contributed by Stefan O'Rear, 5-Feb-2015.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 ⊆ 𝐶) | ||
Theorem | ssrexf 3628 | restricted existential quantification follows from a subclass relationship. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ssralv 3629* | Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.) |
⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | ssrexv 3630* | Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.) |
⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ralss 3631* | Restricted universal quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑))) | ||
Theorem | rexss 3632* | Restricted existential quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
Theorem | ss2ab 3633 | Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994.) |
⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | abss 3634* | Class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.) |
⊢ ({𝑥 ∣ 𝜑} ⊆ 𝐴 ↔ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴)) | ||
Theorem | ssab 3635* | Subclass of a class abstraction. (Contributed by NM, 16-Aug-2006.) |
⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | ssabral 3636* | The relation for a subclass of a class abstraction is equivalent to restricted quantification. (Contributed by NM, 6-Sep-2006.) |
⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ss2abi 3637 | Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} | ||
Theorem | ss2abdv 3638* | Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒}) | ||
Theorem | abssdv 3639* | Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) |
⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴) | ||
Theorem | abssi 3640* | Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) |
⊢ (𝜑 → 𝑥 ∈ 𝐴) ⇒ ⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴 | ||
Theorem | ss2rab 3641 | Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) | ||
Theorem | rabss 3642* | Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵)) | ||
Theorem | ssrab 3643* | Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.) |
⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ssrabdv 3644* | Subclass of a restricted class abstraction (deduction rule). (Contributed by NM, 31-Aug-2006.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
Theorem | rabssdv 3645* | Subclass of a restricted class abstraction (deduction rule). (Contributed by NM, 2-Feb-2015.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵) | ||
Theorem | ss2rabdv 3646* | Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | ss2rabi 3647 | Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabss2 3648* | Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | ssab2 3649* | Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995.) |
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 | ||
Theorem | ssrab2 3650* | Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 | ||
Theorem | ssrabeq 3651* | 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 3652 | A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} | ||
Theorem | uniiunlem 3653* | A subset relationship useful for converting union to indexed union using dfiun2 4490 or dfiun2g 4488 and intersection to indexed intersection using dfiin2 4491. (Contributed by NM, 5-Oct-2006.) (Proof shortened by Mario Carneiro, 26-Sep-2015.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 → (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐶)) | ||
Theorem | dfpss2 3654 | Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | ||
Theorem | dfpss3 3655 | Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴)) | ||
Theorem | psseq1 3656 | Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) | ||
Theorem | psseq2 3657 | Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)) | ||
Theorem | psseq1i 3658 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶) | ||
Theorem | psseq2i 3659 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵) | ||
Theorem | psseq12i 3660 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷) | ||
Theorem | psseq1d 3661 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) | ||
Theorem | psseq2d 3662 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)) | ||
Theorem | psseq12d 3663 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷)) | ||
Theorem | pssss 3664 | A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | ||
Theorem | pssne 3665 | Two classes in a proper subclass relationship are not equal. (Contributed by NM, 16-Feb-2015.) |
⊢ (𝐴 ⊊ 𝐵 → 𝐴 ≠ 𝐵) | ||
Theorem | pssssd 3666 | Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.) |
⊢ (𝜑 → 𝐴 ⊊ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | pssned 3667 | Proper subclasses are unequal. Deduction form of pssne 3665. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊊ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | sspss 3668 | Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) | ||
Theorem | pssirr 3669 | Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) |
⊢ ¬ 𝐴 ⊊ 𝐴 | ||
Theorem | pssn2lp 3670 | 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 3671 | Two ways of stating trichotomy with respect to inclusion. (Contributed by NM, 12-Aug-2004.) |
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴)) | ||
Theorem | ssnpss 3672 | Partial trichotomy law for subclasses. (Contributed by NM, 16-May-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → ¬ 𝐵 ⊊ 𝐴) | ||
Theorem | psstr 3673 | Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) |
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶) | ||
Theorem | sspsstr 3674 | Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶) | ||
Theorem | psssstr 3675 | Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.) |
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊊ 𝐶) | ||
Theorem | psstrd 3676 | Proper subclass inclusion is transitive. Deduction form of psstr 3673. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊊ 𝐵) & ⊢ (𝜑 → 𝐵 ⊊ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐶) | ||
Theorem | sspsstrd 3677 | Transitivity involving subclass and proper subclass inclusion. Deduction form of sspsstr 3674. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊊ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐶) | ||
Theorem | psssstrd 3678 | Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 3675. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊊ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐶) | ||
Theorem | npss 3679 | A class is not a proper subclass of another iff it satisfies a one-directional form of eqss 3583. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (¬ 𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 → 𝐴 = 𝐵)) | ||
Theorem | ssnelpss 3680 | A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002.) |
⊢ (𝐴 ⊆ 𝐵 → ((𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴) → 𝐴 ⊊ 𝐵)) | ||
Theorem | ssnelpssd 3681 | Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 3680. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐵) | ||
Theorem | ssexnelpss 3682* | 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 | difeq1 3683 | Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) | ||
Theorem | difeq2 3684 | Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) | ||
Theorem | difeq12 3685 | Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)) | ||
Theorem | difeq1i 3686 | Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶) | ||
Theorem | difeq2i 3687 | Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵) | ||
Theorem | difeq12i 3688 | Equality inference for class difference. (Contributed by NM, 29-Aug-2004.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷) | ||
Theorem | difeq1d 3689 | Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) | ||
Theorem | difeq2d 3690 | Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) | ||
Theorem | difeq12d 3691 | Equality deduction for class difference. (Contributed by FL, 29-May-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)) | ||
Theorem | difeqri 3692* | Inference from membership to difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ⇒ ⊢ (𝐴 ∖ 𝐵) = 𝐶 | ||
Theorem | nfdif 3693 | Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵) | ||
Theorem | eldifi 3694 | Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵) | ||
Theorem | eldifn 3695 | Implication of membership in a class difference. (Contributed by NM, 3-May-1994.) |
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | elndif 3696 | A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.) |
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ 𝐵)) | ||
Theorem | neldif 3697 | Implication of membership in a class difference. (Contributed by NM, 28-Jun-1994.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ (𝐵 ∖ 𝐶)) → 𝐴 ∈ 𝐶) | ||
Theorem | difdif 3698 | Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.) |
⊢ (𝐴 ∖ (𝐵 ∖ 𝐴)) = 𝐴 | ||
Theorem | difss 3699 | Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴 | ||
Theorem | difssd 3700 | A difference of two classes is contained in the minuend. Deduction form of difss 3699. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |