P. 42 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4101-4200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	psseq1i 4101	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)
Theorem	psseq2i 4102	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)
Theorem	psseq12i 4103	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷)
Theorem	psseq1d 4104	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))
Theorem	psseq2d 4105	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))
Theorem	psseq12d 4106	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷))
Theorem	pssss 4107	A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵)
Theorem	pssne 4108	Two classes in a proper subclass relationship are not equal. (Contributed by NM, 16-Feb-2015.)
⊢ (𝐴 ⊊ 𝐵 → 𝐴 ≠ 𝐵)
Theorem	pssssd 4109	Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	pssned 4110	Proper subclasses are unequal. Deduction form of pssne 4108. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	sspss 4111	Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵))
Theorem	pssirr 4112	Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ ¬ 𝐴 ⊊ 𝐴
Theorem	pssn2lp 4113	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 4114	Two ways of stating trichotomy with respect to inclusion. (Contributed by NM, 12-Aug-2004.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴))
Theorem	ssnpss 4115	Partial trichotomy law for subclasses. (Contributed by NM, 16-May-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → ¬ 𝐵 ⊊ 𝐴)
Theorem	psstr 4116	Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶)
Theorem	sspsstr 4117	Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶)
Theorem	psssstr 4118	Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊊ 𝐶)
Theorem	psstrd 4119	Proper subclass inclusion is transitive. Deduction form of psstr 4116. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊊ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐶)
Theorem	sspsstrd 4120	Transitivity involving subclass and proper subclass inclusion. Deduction form of sspsstr 4117. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊊ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐶)
Theorem	psssstrd 4121	Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 4118. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐶)
Theorem	npss 4122	A class is not a proper subclass of another iff it satisfies a one-directional form of eqss 4010. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (¬ 𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 → 𝐴 = 𝐵))
Theorem	ssnelpss 4123	A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002.)
⊢ (𝐴 ⊆ 𝐵 → ((𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴) → 𝐴 ⊊ 𝐵))
Theorem	ssnelpssd 4124	Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 4123. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐵)
Theorem	ssexnelpss 4125*	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 4126*	Alternate definition of class difference. (Contributed by BJ and Jim Kingdon, 16-Jun-2022.) (Proof shortened by SN, 15-Aug-2025.)
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦}
Theorem	dfdif3OLD 4127*	Obsolete version of dfdif3 4126 as of 15-Aug-2025. (Contributed by BJ and Jim Kingdon, 16-Jun-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦}
Theorem	difeq1 4128	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
Theorem	difeq2 4129	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
Theorem	difeq12 4130	Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷))
Theorem	difeq1i 4131	Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)
Theorem	difeq2i 4132	Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)
Theorem	difeq12i 4133	Equality inference for class difference. (Contributed by NM, 29-Aug-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)
Theorem	difeq1d 4134	Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
Theorem	difeq2d 4135	Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
Theorem	difeq12d 4136	Equality deduction for class difference. (Contributed by FL, 29-May-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷))
Theorem	difeqri 4137*	Inference from membership to difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∖ 𝐵) = 𝐶
Theorem	nfdif 4138	Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) Avoid ax-10 2138, ax-11 2154, ax-12 2174. (Revised by SN, 14-May-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)
Theorem	nfdifOLD 4139	Obsolete version of nfdif 4138 as of 14-May-2025. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)
Theorem	eldifi 4140	Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵)
Theorem	eldifn 4141	Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶)
Theorem	elndif 4142	A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ 𝐵))
Theorem	neldif 4143	Implication of membership in a class difference. (Contributed by NM, 28-Jun-1994.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ (𝐵 ∖ 𝐶)) → 𝐴 ∈ 𝐶)
Theorem	difdif 4144	Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.)
⊢ (𝐴 ∖ (𝐵 ∖ 𝐴)) = 𝐴
Theorem	difss 4145	Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
Theorem	difssd 4146	A difference of two classes is contained in the minuend. Deduction form of difss 4145. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴)
Theorem	difss2 4147	If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.)
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → 𝐴 ⊆ 𝐵)
Theorem	difss2d 4148	If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 4147. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	ssdifss 4149	Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵)
Theorem	ddif 4150	Double complement under universal class. Exercise 4.10(s) of [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.)
⊢ (V ∖ (V ∖ 𝐴)) = 𝐴
Theorem	ssconb 4151	Contraposition law for subsets. (Contributed by NM, 22-Mar-1998.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ 𝐵 ⊆ (𝐶 ∖ 𝐴)))
Theorem	sscon 4152	Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))
Theorem	ssdif 4153	Difference law for subsets. (Contributed by NM, 28-May-1998.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
Theorem	ssdifd 4154	If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 4153. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
Theorem	sscond 4155	If 𝐴 is contained in 𝐵, then (𝐶 ∖ 𝐵) is contained in (𝐶 ∖ 𝐴). Deduction form of sscon 4152. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))
Theorem	ssdifssd 4156	If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is also contained in 𝐵. Deduction form of ssdifss 4149. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵)
Theorem	ssdif2d 4157	If 𝐴 is contained in 𝐵 and 𝐶 is contained in 𝐷, then (𝐴 ∖ 𝐷) is contained in (𝐵 ∖ 𝐶). Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ (𝐵 ∖ 𝐶))
Theorem	raldifb 4158	Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018.)
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∉ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ (𝐴 ∖ 𝐵)𝜑)
Theorem	rexdifi 4159	Restricted existential quantification over a difference. (Contributed by AV, 25-Oct-2023.)
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝜑) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)𝜑)
Theorem	complss 4160	Complementation reverses inclusion. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 19-Mar-2021.)
⊢ (𝐴 ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ (V ∖ 𝐴))
Theorem	compleq 4161	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 4162	Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.)
⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))
Theorem	elunnel1 4163	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 4164	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 4165*	Inference from membership to union. (Contributed by NM, 21-Jun-1993.)
⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∪ 𝐵) = 𝐶
Theorem	unidm 4166	Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 21-Jun-1993.)
⊢ (𝐴 ∪ 𝐴) = 𝐴
Theorem	uncom 4167	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 4168	If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom 4168 was automatically derived from equncomVD 44865 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.)
⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵))
Theorem	equncomi 4169	Inference form of equncom 4168. equncomi 4169 was automatically derived from equncomiVD 44866 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.)
⊢ 𝐴 = (𝐵 ∪ 𝐶)    ⇒   ⊢ 𝐴 = (𝐶 ∪ 𝐵)
Theorem	uneq1 4170	Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993.)
⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
Theorem	uneq2 4171	Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
Theorem	uneq12 4172	Equality theorem for the union of two classes. (Contributed by NM, 29-Mar-1998.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
Theorem	uneq1i 4173	Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)
Theorem	uneq2i 4174	Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)
Theorem	uneq12i 4175	Equality inference for the union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)
Theorem	uneq1d 4176	Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
Theorem	uneq2d 4177	Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
Theorem	uneq12d 4178	Equality deduction for the union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
Theorem	nfun 4179	Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) Avoid ax-10 2138, ax-11 2154, ax-12 2174. (Revised by SN, 14-May-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)
Theorem	nfunOLD 4180	Obsolete version of nfun 4179 as of 14-May-2025. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)
Theorem	unass 4181	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 4182	A rearrangement of union. (Contributed by NM, 12-Aug-2004.)
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (𝐴 ∪ 𝐶))
Theorem	un23 4183	A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ 𝐵)
Theorem	un4 4184	A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∪ (𝐶 ∪ 𝐷)) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐷))
Theorem	unundi 4185	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∪ (𝐴 ∪ 𝐶))
Theorem	unundir 4186	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐶))
Theorem	ssun1 4187	Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
Theorem	ssun2 4188	Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)
Theorem	ssun3 4189	Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐵 ∪ 𝐶))
Theorem	ssun4 4190	Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐶 ∪ 𝐵))
Theorem	elun1 4191	Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))
Theorem	elun2 4192	Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))
Theorem	elunant 4193	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 4194	Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶))
Theorem	ssequn1 4195	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 4196	Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∪ 𝐴) ⊆ (𝐶 ∪ 𝐵))
Theorem	unss12 4197	Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷))
Theorem	ssequn2 4198	A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
Theorem	unss 4199	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 4200	An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.)
⊢ 𝐴 ⊆ 𝐶    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶