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	rexss 4001*	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 4002*	Obsolete version of ralss 4000 as of 14-Oct-2025. (Contributed by Stefan O'Rear, 3-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑)))
Theorem	rexssOLD 4003*	Obsolete version of rexss 4001 as of 14-Oct-2025. (Contributed by Stefan O'Rear, 3-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑)))
Theorem	ss2abim 4004	Class abstractions in a subclass relationship. Reverse direction of ss2ab 4005 which requires fewer axioms. (Contributed by SN, 22-Dec-2024.)
⊢ (∀𝑥(𝜑 → 𝜓) → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
Theorem	ss2ab 4005	Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994.)
⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 → 𝜓))
Theorem	abss 4006*	Class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
⊢ ({𝑥 ∣ 𝜑} ⊆ 𝐴 ↔ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴))
Theorem	ssab 4007*	Subclass of a class abstraction. (Contributed by NM, 16-Aug-2006.)
⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
Theorem	ssabral 4008*	The relation for a subclass of a class abstraction is equivalent to restricted quantification. (Contributed by NM, 6-Sep-2006.)
⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	ss2abdv 4009*	Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 28-Jun-2024.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})
Theorem	ss2abi 4010	Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2134, ax-10 2165, ax-11 2181, ax-12 2202. (Revised by GG, 28-Jun-2024.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓}
Theorem	abssdv 4011*	Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) (Proof shortened by SN, 22-Dec-2024.)
⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴)
Theorem	abssi 4012*	Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    ⇒   ⊢ {𝑥 ∣ 𝜑} ⊆ 𝐴
Theorem	ss2rab 4013	Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
Theorem	rabss 4014*	Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵))
Theorem	ssrab 4015*	Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.)
⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	ss2rabd 4016	Subclass of a restricted class abstraction (deduction form). Saves ax-10 2165, ax-11 2181, ax-12 2202 over using ss2rab 4013 and sylibr 236. (Contributed by SN, 4-Feb-2026.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	ssrabdv 4017*	Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 31-Aug-2006.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝜓)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓})
Theorem	rabssdv 4018*	Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 2-Feb-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵)
Theorem	ss2rabdv 4019*	Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.) Avoid axioms. (Revised by TM, 1-Feb-2026.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	ss2rabi 4020	Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.) Avoid axioms. (Revised by SN, 4-Feb-2025.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabss2 4021*	Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid axioms. (Revised by TM, 1-Feb-2026.)
⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑})
Theorem	rabss2OLD 4022*	Obsolete version of rabss2 4021 as of 1-Feb-2026. (Contributed by NM, 30-May-2006.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑})
Theorem	ssab2 4023*	Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995.)
⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴
Theorem	ssrab2 4024*	Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.) (Proof shortened by BJ and SN, 8-Aug-2024.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
Theorem	rabss3d 4025*	Subclass law for restricted abstraction. (Contributed by Thierry Arnoux, 25-Sep-2017.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	ssrab3 4026*	Subclass relation for a restricted class abstraction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    ⇒   ⊢ 𝐵 ⊆ 𝐴
Theorem	rabssrabd 4027*	Subclass of a restricted class abstraction. (Contributed by AV, 4-Jun-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝑥 ∈ 𝐴) → 𝜒)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	ssrabeq 4028*	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 4029	A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑}
Theorem	eqrrabd 4030*	Deduce equality with a restricted abstraction. (Contributed by Thierry Arnoux, 11-Apr-2024.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓))    ⇒   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓})
Theorem	uniiunlem 4031*	A subset relationship useful for converting union to indexed union using dfiun2 4979 or dfiun2g 4977 and intersection to indexed intersection using dfiin2 4980. (Contributed by NM, 5-Oct-2006.) (Proof shortened by Mario Carneiro, 26-Sep-2015.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 → (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐶))
Theorem	dfpss2 4032	Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.)
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
Theorem	dfpss3 4033	Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴))
Theorem	psseq1 4034	Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)
⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))
Theorem	psseq2 4035	Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)
⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))
Theorem	psseq1i 4036	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)
Theorem	psseq2i 4037	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)
Theorem	psseq12i 4038	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷)
Theorem	psseq1d 4039	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))
Theorem	psseq2d 4040	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))
Theorem	psseq12d 4041	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷))
Theorem	pssss 4042	A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵)
Theorem	pssne 4043	Two classes in a proper subclass relationship are not equal. (Contributed by NM, 16-Feb-2015.)
⊢ (𝐴 ⊊ 𝐵 → 𝐴 ≠ 𝐵)
Theorem	pssssd 4044	Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	pssned 4045	Proper subclasses are unequal. Deduction form of pssne 4043. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	sspss 4046	Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵))
Theorem	pssirr 4047	Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ ¬ 𝐴 ⊊ 𝐴
Theorem	pssirrOLD 4048	Obsolete version of pssirr 4047 as of 10-Jun-2026. (Contributed by NM, 7-Feb-1996.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝐴 ⊊ 𝐴
Theorem	pssn2lp 4049	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 4050	Two ways of stating trichotomy with respect to inclusion. (Contributed by NM, 12-Aug-2004.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴))
Theorem	ssnpss 4051	Partial trichotomy law for subclasses. (Contributed by NM, 16-May-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → ¬ 𝐵 ⊊ 𝐴)
Theorem	psstr 4052	Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶)
Theorem	sspsstr 4053	Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶)
Theorem	psssstr 4054	Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊊ 𝐶)
Theorem	psstrd 4055	Proper subclass inclusion is transitive. Deduction form of psstr 4052. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊊ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐶)
Theorem	sspsstrd 4056	Transitivity involving subclass and proper subclass inclusion. Deduction form of sspsstr 4053. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊊ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐶)
Theorem	psssstrd 4057	Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 4054. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐶)
Theorem	npss 4058	A class is not a proper subclass of another iff it satisfies a one-directional form of eqss 3942. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (¬ 𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 → 𝐴 = 𝐵))
Theorem	ssnelpss 4059	A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002.)
⊢ (𝐴 ⊆ 𝐵 → ((𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴) → 𝐴 ⊊ 𝐵))
Theorem	ssnelpssd 4060	Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 4059. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐵)
Theorem	ssexnelpss 4061*	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.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝑥 ∉ 𝐴) → 𝐴 ⊊ 𝐵)
2.1.13  The difference, union, and intersection of two classes
2.1.13.1  The difference of two classes
Theorem	dfdif3 4062*	Alternate definition of class difference. (Contributed by BJ and Jim Kingdon, 16-Jun-2022.) (Proof shortened by SN, 15-Aug-2025.)
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦}
Theorem	dfdif3OLD 4063*	Obsolete version of dfdif3 4062 as of 15-Aug-2025. (Contributed by BJ and Jim Kingdon, 16-Jun-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦}
Theorem	difeq1 4064	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
Theorem	difeq2 4065	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
Theorem	difeq12 4066	Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷))
Theorem	difeq1i 4067	Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)
Theorem	difeq2i 4068	Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)
Theorem	difeq12i 4069	Equality inference for class difference. (Contributed by NM, 29-Aug-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)
Theorem	difeq1d 4070	Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
Theorem	difeq2d 4071	Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
Theorem	difeq12d 4072	Equality deduction for class difference. (Contributed by FL, 29-May-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷))
Theorem	difeqri 4073*	Inference from membership to difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∖ 𝐵) = 𝐶
Theorem	nfdif 4074	Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) Avoid ax-10 2165, ax-11 2181, ax-12 2202. (Revised by SN, 14-May-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)
Theorem	eldifi 4075	Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵)
Theorem	eldifn 4076	Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶)
Theorem	elndif 4077	A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ 𝐵))
Theorem	neldif 4078	Implication of membership in a class difference. (Contributed by NM, 28-Jun-1994.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ (𝐵 ∖ 𝐶)) → 𝐴 ∈ 𝐶)
Theorem	difdif 4079	Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.)
⊢ (𝐴 ∖ (𝐵 ∖ 𝐴)) = 𝐴
Theorem	difss 4080	Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
Theorem	difssd 4081	A difference of two classes is contained in the minuend. Deduction form of difss 4080. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴)
Theorem	difss2 4082	If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.)
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → 𝐴 ⊆ 𝐵)
Theorem	difss2d 4083	If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 4082. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	ssdifss 4084	Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵)
Theorem	ddif 4085	Double complement under universal class. Exercise 4.10(s) of [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.)
⊢ (V ∖ (V ∖ 𝐴)) = 𝐴
Theorem	ssconb 4086	Contraposition law for subsets. (Contributed by NM, 22-Mar-1998.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ 𝐵 ⊆ (𝐶 ∖ 𝐴)))
Theorem	sscon 4087	Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))
Theorem	ssdif 4088	Difference law for subsets. (Contributed by NM, 28-May-1998.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
Theorem	ssdifd 4089	If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 4088. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
Theorem	sscond 4090	If 𝐴 is contained in 𝐵, then (𝐶 ∖ 𝐵) is contained in (𝐶 ∖ 𝐴). Deduction form of sscon 4087. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))
Theorem	ssdifssd 4091	If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is also contained in 𝐵. Deduction form of ssdifss 4084. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵)
Theorem	ssdif2d 4092	If 𝐴 is contained in 𝐵 and 𝐶 is contained in 𝐷, then (𝐴 ∖ 𝐷) is contained in (𝐵 ∖ 𝐶). Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ (𝐵 ∖ 𝐶))
Theorem	raldifb 4093	Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018.)
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∉ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ (𝐴 ∖ 𝐵)𝜑)
Theorem	rexdifi 4094	Restricted existential quantification over a difference. (Contributed by AV, 25-Oct-2023.)
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝜑) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)𝜑)
Theorem	complss 4095	Complementation reverses inclusion. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 19-Mar-2021.)
⊢ (𝐴 ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ (V ∖ 𝐴))
Theorem	compleq 4096	Two classes are equal if and only if their complements are equal. (Contributed by BJ, 19-Mar-2021.)
⊢ (𝐴 = 𝐵 ↔ (V ∖ 𝐴) = (V ∖ 𝐵))
2.1.13.2  The union of two classes
Theorem	elun 4097	Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.)
⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))
Theorem	elunnel1 4098	A member of a union that is not a member of the first class, is a member of the second class. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ (𝐵 ∪ 𝐶) ∧ ¬ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐶)
Theorem	elunnel2 4099	A member of a union that is not a member of the second class, is a member of the first class. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ (𝐵 ∪ 𝐶) ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ 𝐵)
Theorem	uneqri 4100*	Inference from membership to union. (Contributed by NM, 21-Jun-1993.)
⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∪ 𝐵) = 𝐶