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