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