P. 41 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4001-4100   *Has distinct variable group(s)

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.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)