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	pssss 4001	A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵)
Theorem	pssne 4002	Two classes in a proper subclass relationship are not equal. (Contributed by NM, 16-Feb-2015.)
⊢ (𝐴 ⊊ 𝐵 → 𝐴 ≠ 𝐵)
Theorem	pssssd 4003	Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	pssned 4004	Proper subclasses are unequal. Deduction form of pssne 4002. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	sspss 4005	Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵))
Theorem	pssirr 4006	Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ ¬ 𝐴 ⊊ 𝐴
Theorem	pssn2lp 4007	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 4008	Two ways of stating trichotomy with respect to inclusion. (Contributed by NM, 12-Aug-2004.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴))
Theorem	ssnpss 4009	Partial trichotomy law for subclasses. (Contributed by NM, 16-May-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → ¬ 𝐵 ⊊ 𝐴)
Theorem	psstr 4010	Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶)
Theorem	sspsstr 4011	Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶)
Theorem	psssstr 4012	Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊊ 𝐶)
Theorem	psstrd 4013	Proper subclass inclusion is transitive. Deduction form of psstr 4010. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊊ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐶)
Theorem	sspsstrd 4014	Transitivity involving subclass and proper subclass inclusion. Deduction form of sspsstr 4011. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊊ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐶)
Theorem	psssstrd 4015	Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 4012. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐶)
Theorem	npss 4016	A class is not a proper subclass of another iff it satisfies a one-directional form of eqss 3907. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (¬ 𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 → 𝐴 = 𝐵))
Theorem	ssnelpss 4017	A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002.)
⊢ (𝐴 ⊆ 𝐵 → ((𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴) → 𝐴 ⊊ 𝐵))
Theorem	ssnelpssd 4018	Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 4017. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐵)
Theorem	ssexnelpss 4019*	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 4020*	Alternate definition of class difference. (Contributed by BJ and Jim Kingdon, 16-Jun-2022.)
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦}
Theorem	difeq1 4021	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
Theorem	difeq2 4022	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
Theorem	difeq12 4023	Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷))
Theorem	difeq1i 4024	Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)
Theorem	difeq2i 4025	Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)
Theorem	difeq12i 4026	Equality inference for class difference. (Contributed by NM, 29-Aug-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)
Theorem	difeq1d 4027	Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
Theorem	difeq2d 4028	Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
Theorem	difeq12d 4029	Equality deduction for class difference. (Contributed by FL, 29-May-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷))
Theorem	difeqri 4030*	Inference from membership to difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∖ 𝐵) = 𝐶
Theorem	nfdif 4031	Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)
Theorem	eldifi 4032	Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵)
Theorem	eldifn 4033	Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶)
Theorem	elndif 4034	A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ 𝐵))
Theorem	neldif 4035	Implication of membership in a class difference. (Contributed by NM, 28-Jun-1994.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ (𝐵 ∖ 𝐶)) → 𝐴 ∈ 𝐶)
Theorem	difdif 4036	Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.)
⊢ (𝐴 ∖ (𝐵 ∖ 𝐴)) = 𝐴
Theorem	difss 4037	Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
Theorem	difssd 4038	A difference of two classes is contained in the minuend. Deduction form of difss 4037. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴)
Theorem	difss2 4039	If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.)
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → 𝐴 ⊆ 𝐵)
Theorem	difss2d 4040	If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 4039. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	ssdifss 4041	Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵)
Theorem	ddif 4042	Double complement under universal class. Exercise 4.10(s) of [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.)
⊢ (V ∖ (V ∖ 𝐴)) = 𝐴
Theorem	ssconb 4043	Contraposition law for subsets. (Contributed by NM, 22-Mar-1998.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ 𝐵 ⊆ (𝐶 ∖ 𝐴)))
Theorem	sscon 4044	Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))
Theorem	ssdif 4045	Difference law for subsets. (Contributed by NM, 28-May-1998.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
Theorem	ssdifd 4046	If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 4045. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
Theorem	sscond 4047	If 𝐴 is contained in 𝐵, then (𝐶 ∖ 𝐵) is contained in (𝐶 ∖ 𝐴). Deduction form of sscon 4044. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))
Theorem	ssdifssd 4048	If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is also contained in 𝐵. Deduction form of ssdifss 4041. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵)
Theorem	ssdif2d 4049	If 𝐴 is contained in 𝐵 and 𝐶 is contained in 𝐷, then (𝐴 ∖ 𝐷) is contained in (𝐵 ∖ 𝐶). Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ (𝐵 ∖ 𝐶))
Theorem	raldifb 4050	Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018.)
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∉ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ (𝐴 ∖ 𝐵)𝜑)
Theorem	rexdifi 4051	Restricted existential quantification over a difference. (Contributed by AV, 25-Oct-2023.)
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝜑) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)𝜑)
Theorem	complss 4052	Complementation reverses inclusion. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 19-Mar-2021.)
⊢ (𝐴 ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ (V ∖ 𝐴))
Theorem	compleq 4053	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 4054	Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.)
⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))
Theorem	elunnel1 4055	A member of a union that is not member of the first class, is member of the second class. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ (𝐵 ∪ 𝐶) ∧ ¬ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐶)
Theorem	uneqri 4056*	Inference from membership to union. (Contributed by NM, 21-Jun-1993.)
⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∪ 𝐵) = 𝐶
Theorem	unidm 4057	Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 21-Jun-1993.)
⊢ (𝐴 ∪ 𝐴) = 𝐴
Theorem	uncom 4058	Commutative law for union of classes. Exercise 6 of [TakeutiZaring] p. 17. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
Theorem	equncom 4059	If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom 4059 was automatically derived from equncomVD 41947 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.)
⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵))
Theorem	equncomi 4060	Inference form of equncom 4059. equncomi 4060 was automatically derived from equncomiVD 41948 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.)
⊢ 𝐴 = (𝐵 ∪ 𝐶)    ⇒   ⊢ 𝐴 = (𝐶 ∪ 𝐵)
Theorem	uneq1 4061	Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993.)
⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
Theorem	uneq2 4062	Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
Theorem	uneq12 4063	Equality theorem for the union of two classes. (Contributed by NM, 29-Mar-1998.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
Theorem	uneq1i 4064	Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)
Theorem	uneq2i 4065	Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)
Theorem	uneq12i 4066	Equality inference for the union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)
Theorem	uneq1d 4067	Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
Theorem	uneq2d 4068	Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
Theorem	uneq12d 4069	Equality deduction for the union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
Theorem	nfun 4070	Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)
Theorem	unass 4071	Associative law for union of classes. Exercise 8 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵 ∪ 𝐶))
Theorem	un12 4072	A rearrangement of union. (Contributed by NM, 12-Aug-2004.)
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (𝐴 ∪ 𝐶))
Theorem	un23 4073	A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ 𝐵)
Theorem	un4 4074	A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∪ (𝐶 ∪ 𝐷)) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐷))
Theorem	unundi 4075	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∪ (𝐴 ∪ 𝐶))
Theorem	unundir 4076	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐶))
Theorem	ssun1 4077	Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
Theorem	ssun2 4078	Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)
Theorem	ssun3 4079	Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐵 ∪ 𝐶))
Theorem	ssun4 4080	Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐶 ∪ 𝐵))
Theorem	elun1 4081	Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))
Theorem	elun2 4082	Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))
Theorem	elunant 4083	A statement is true for every element of the union of a pair of classes if and only if it is true for every element of the first class and for every element of the second class. (Contributed by BTernaryTau, 27-Sep-2023.)
⊢ ((𝐶 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝐶 ∈ 𝐴 → 𝜑) ∧ (𝐶 ∈ 𝐵 → 𝜑)))
Theorem	unss1 4084	Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶))
Theorem	ssequn1 4085	A relationship between subclass and union. Theorem 26 of [Suppes] p. 27. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
Theorem	unss2 4086	Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∪ 𝐴) ⊆ (𝐶 ∪ 𝐵))
Theorem	unss12 4087	Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷))
Theorem	ssequn2 4088	A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
Theorem	unss 4089	The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse. (Contributed by NM, 11-Jun-2004.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
Theorem	unssi 4090	An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.)
⊢ 𝐴 ⊆ 𝐶    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶
Theorem	unssd 4091	A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)
Theorem	unssad 4092	If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4089. Partial converse of unssd 4091. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	unssbd 4093	If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 4089. Partial converse of unssd 4091. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
Theorem	ssun 4094	A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶) → 𝐴 ⊆ (𝐵 ∪ 𝐶))
Theorem	rexun 4095	Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑))
Theorem	ralunb 4096	Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	ralun 4097	Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑)
2.1.13.3  The intersection of two classes
Theorem	elini 4098	Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐴 ∈ 𝐶    ⇒   ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶)
Theorem	elind 4099	Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))
Theorem	elinel1 4100	Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵)