| Metamath
Proof Explorer Theorem List (p. 41 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | eqssd 4001 | Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | sssseq 4002 | 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 4003 | Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017.) (Proof shortened by BJ, 1-Dec-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | eqri 4004 | Infer equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 7-Oct-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ⇒ ⊢ 𝐴 = 𝐵 | ||
| Theorem | eqelssd 4005* | Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | ssid 4006 | 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 4007 | Weakening of ssid 4006. (Contributed by BJ, 1-Sep-2022.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐴) | ||
| Theorem | ssv 4008 | Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.) |
| ⊢ 𝐴 ⊆ V | ||
| Theorem | sseq1 4009 | Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
| ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | ||
| Theorem | sseq2 4010 | Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.) |
| ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | ||
| Theorem | sseq12 4011 | Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.) |
| ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)) | ||
| Theorem | sseq1i 4012 | An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) | ||
| Theorem | sseq2i 4013 | An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) | ||
| Theorem | sseq12i 4014 | An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷) | ||
| Theorem | sseq1d 4015 | An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | ||
| Theorem | sseq2d 4016 | An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | ||
| Theorem | sseq12d 4017 | An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)) | ||
| Theorem | eqsstrd 4018 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
| Theorem | eqsstrrd 4019 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
| ⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
| Theorem | sseqtrd 4020 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
| Theorem | sseqtrrd 4021 | Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
| Theorem | eqsstrid 4022 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
| Theorem | eqsstrrid 4023 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
| ⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
| Theorem | sseqtrdi 4024 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
| Theorem | sseqtrrdi 4025 | A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
| Theorem | sseqtrid 4026 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| ⊢ 𝐵 ⊆ 𝐴 & ⊢ (𝜑 → 𝐴 = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | ||
| Theorem | sseqtrrid 4027 | Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| ⊢ 𝐵 ⊆ 𝐴 & ⊢ (𝜑 → 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | ||
| Theorem | eqsstrdi 4028 | A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
| Theorem | eqsstrrdi 4029 | A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
| Theorem | eqsstri 4030 | Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
| Theorem | eqsstrri 4031 | Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.) |
| ⊢ 𝐵 = 𝐴 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
| Theorem | sseqtri 4032 | Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.) |
| ⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
| Theorem | sseqtrri 4033 | Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.) |
| ⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ⊆ 𝐶 | ||
| Theorem | 3sstr3i 4034 | 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 4035 | 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 4036 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ⊆ 𝐷) | ||
| Theorem | 3sstr4g 4037 | 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 4038 | Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶 ⊆ 𝐷) | ||
| Theorem | 3sstr4d 4039 | 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 | eqimssd 4040 | Equality implies inclusion, deduction version. (Contributed by SN, 6-Nov-2024.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
| Theorem | eqimsscd 4041 | Equality implies inclusion, deduction version. (Contributed by SN, 15-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐴) | ||
| Theorem | eqimss 4042 | Equality implies inclusion. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
| ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | ||
| Theorem | eqimss2 4043 | Equality implies inclusion. (Contributed by NM, 23-Nov-2003.) |
| ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵) | ||
| Theorem | eqimssi 4044 | Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
| Theorem | eqimss2i 4045 | Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝐵 ⊆ 𝐴 | ||
| Theorem | nssne1 4046 | Two classes are different if they don't include the same class. (Contributed by NM, 23-Apr-2015.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ⊆ 𝐶) → 𝐵 ≠ 𝐶) | ||
| Theorem | nssne2 4047 | Two classes are different if they are not subclasses of the same class. (Contributed by NM, 23-Apr-2015.) |
| ⊢ ((𝐴 ⊆ 𝐶 ∧ ¬ 𝐵 ⊆ 𝐶) → 𝐴 ≠ 𝐵) | ||
| Theorem | nss 4048* | 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 4049 | Demonstrate by witnesses that two classes lack a subclass relation. (Contributed by Stefan O'Rear, 5-Feb-2015.) |
| ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 ⊆ 𝐶) | ||
| Theorem | ssrexf 4050 | Restricted existential quantification follows from a subclass relationship. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) | ||
| Theorem | ssrmof 4051 | "At most one" existential quantification restricted to a subclass. (Contributed by Thierry Arnoux, 8-Oct-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 → (∃*𝑥 ∈ 𝐵 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)) | ||
| Theorem | ssralv 4052* | Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.) Avoid axioms. (Revised by GG, 19-May-2025.) |
| ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑)) | ||
| Theorem | ssrexv 4053* | Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.) Avoid axioms. (Revised by GG, 19-May-2025.) |
| ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) | ||
| Theorem | ss2ralv 4054* | Two quantifications restricted to a subclass. (Contributed by AV, 11-Mar-2023.) |
| ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑)) | ||
| Theorem | ss2rexv 4055* | Two existential quantifications restricted to a subclass. (Contributed by AV, 11-Mar-2023.) |
| ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝜑)) | ||
| Theorem | ssralvOLD 4056* | Obsolete version of ssralv 4052 as of 19-May-2025. (Contributed by NM, 11-Mar-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑)) | ||
| Theorem | ssrexvOLD 4057* | Obsolete version of ssrexv 4053 as of 19-May-2025. (Contributed by NM, 11-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑)) | ||
| Theorem | ralss 4058* | Restricted universal quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.) Avoid axioms. (Revised by SN, 14-Oct-2025.) |
| ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑))) | ||
| Theorem | rexss 4059* | Restricted existential quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.) Avoid axioms. (Revised by SN, 14-Oct-2025.) |
| ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
| Theorem | ralssOLD 4060* | Obsolete version of ralss 4058 as of 14-Oct-2025. (Contributed by Stefan O'Rear, 3-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑))) | ||
| Theorem | rexssOLD 4061* | Obsolete version of rexss 4059 as of 14-Oct-2025. (Contributed by Stefan O'Rear, 3-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
| Theorem | ss2ab 4062 | Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994.) |
| ⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 → 𝜓)) | ||
| Theorem | abss 4063* | Class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.) |
| ⊢ ({𝑥 ∣ 𝜑} ⊆ 𝐴 ↔ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴)) | ||
| Theorem | ssab 4064* | Subclass of a class abstraction. (Contributed by NM, 16-Aug-2006.) |
| ⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | ||
| Theorem | ssabral 4065* | The relation for a subclass of a class abstraction is equivalent to restricted quantification. (Contributed by NM, 6-Sep-2006.) |
| ⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
| Theorem | ss2abdv 4066* | Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) (Revised by Steven Nguyen, 28-Jun-2024.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒}) | ||
| Theorem | ss2abi 4067 | Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2110, ax-10 2141, ax-11 2157, ax-12 2177. (Revised by GG, 28-Jun-2024.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} | ||
| Theorem | abssdv 4068* | Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) (Proof shortened by SN, 22-Dec-2024.) |
| ⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴) | ||
| Theorem | abssdvOLD 4069* | Obsolete version of abssdv 4068 as of 12-Dec-2024. (Contributed by NM, 20-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴) | ||
| Theorem | abssi 4070* | Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) |
| ⊢ (𝜑 → 𝑥 ∈ 𝐴) ⇒ ⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴 | ||
| Theorem | ss2rab 4071 | Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) | ||
| Theorem | rabss 4072* | Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵)) | ||
| Theorem | ssrab 4073* | Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.) |
| ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | ||
| Theorem | ssrabdv 4074* | Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 31-Aug-2006.) |
| ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
| Theorem | rabssdv 4075* | Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 2-Feb-2015.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵) | ||
| Theorem | ss2rabdv 4076* | Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
| Theorem | ss2rabi 4077 | Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.) |
| ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
| Theorem | rabss2 4078* | Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
| Theorem | ssab2 4079* | Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995.) |
| ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 | ||
| Theorem | ssrab2 4080* | Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.) (Proof shortened by BJ and SN, 8-Aug-2024.) |
| ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 | ||
| Theorem | rabss3d 4081* | Subclass law for restricted abstraction. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
| ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
| Theorem | ssrab3 4082* | Subclass relation for a restricted class abstraction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} ⇒ ⊢ 𝐵 ⊆ 𝐴 | ||
| Theorem | rabssrabd 4083* | Subclass of a restricted class abstraction. (Contributed by AV, 4-Jun-2022.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝑥 ∈ 𝐴) → 𝜒) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
| Theorem | ssrabeq 4084* | 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 4085 | A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016.) |
| ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} | ||
| Theorem | eqrrabd 4086* | Deduce equality with a restricted abstraction. (Contributed by Thierry Arnoux, 11-Apr-2024.) |
| ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
| Theorem | uniiunlem 4087* | A subset relationship useful for converting union to indexed union using dfiun2 5033 or dfiun2g 5030 and intersection to indexed intersection using dfiin2 5034. (Contributed by NM, 5-Oct-2006.) (Proof shortened by Mario Carneiro, 26-Sep-2015.) |
| ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 → (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐶)) | ||
| Theorem | dfpss2 4088 | Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) |
| ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | ||
| Theorem | dfpss3 4089 | Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴)) | ||
| Theorem | psseq1 4090 | Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.) |
| ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) | ||
| Theorem | psseq2 4091 | Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.) |
| ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)) | ||
| Theorem | psseq1i 4092 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶) | ||
| Theorem | psseq2i 4093 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵) | ||
| Theorem | psseq12i 4094 | An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷) | ||
| Theorem | psseq1d 4095 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) | ||
| Theorem | psseq2d 4096 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)) | ||
| Theorem | psseq12d 4097 | An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷)) | ||
| Theorem | pssss 4098 | A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) |
| ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | ||
| Theorem | pssne 4099 | Two classes in a proper subclass relationship are not equal. (Contributed by NM, 16-Feb-2015.) |
| ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ≠ 𝐵) | ||
| Theorem | pssssd 4100 | Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.) |
| ⊢ (𝜑 → 𝐴 ⊊ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |