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	psssstrd 4101	Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 4098. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊊ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐶)
Theorem	npss 4102	A class is not a proper subclass of another iff it satisfies a one-directional form of eqss 3989. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (¬ 𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 → 𝐴 = 𝐵))
Theorem	ssnelpss 4103	A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002.)
⊢ (𝐴 ⊆ 𝐵 → ((𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴) → 𝐴 ⊊ 𝐵))
Theorem	ssnelpssd 4104	Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 4103. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ⊊ 𝐵)
Theorem	ssexnelpss 4105*	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 4106*	Alternate definition of class difference. (Contributed by BJ and Jim Kingdon, 16-Jun-2022.)
⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦}
Theorem	difeq1 4107	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
Theorem	difeq2 4108	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
Theorem	difeq12 4109	Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷))
Theorem	difeq1i 4110	Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)
Theorem	difeq2i 4111	Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)
Theorem	difeq12i 4112	Equality inference for class difference. (Contributed by NM, 29-Aug-2004.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)
Theorem	difeq1d 4113	Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
Theorem	difeq2d 4114	Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
Theorem	difeq12d 4115	Equality deduction for class difference. (Contributed by FL, 29-May-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷))
Theorem	difeqri 4116*	Inference from membership to difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∖ 𝐵) = 𝐶
Theorem	nfdif 4117	Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵)
Theorem	eldifi 4118	Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵)
Theorem	eldifn 4119	Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶)
Theorem	elndif 4120	A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ 𝐵))
Theorem	neldif 4121	Implication of membership in a class difference. (Contributed by NM, 28-Jun-1994.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ (𝐵 ∖ 𝐶)) → 𝐴 ∈ 𝐶)
Theorem	difdif 4122	Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.)
⊢ (𝐴 ∖ (𝐵 ∖ 𝐴)) = 𝐴
Theorem	difss 4123	Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
Theorem	difssd 4124	A difference of two classes is contained in the minuend. Deduction form of difss 4123. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴)
Theorem	difss2 4125	If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.)
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → 𝐴 ⊆ 𝐵)
Theorem	difss2d 4126	If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 4125. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	ssdifss 4127	Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵)
Theorem	ddif 4128	Double complement under universal class. Exercise 4.10(s) of [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.)
⊢ (V ∖ (V ∖ 𝐴)) = 𝐴
Theorem	ssconb 4129	Contraposition law for subsets. (Contributed by NM, 22-Mar-1998.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ 𝐵 ⊆ (𝐶 ∖ 𝐴)))
Theorem	sscon 4130	Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))
Theorem	ssdif 4131	Difference law for subsets. (Contributed by NM, 28-May-1998.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
Theorem	ssdifd 4132	If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 4131. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
Theorem	sscond 4133	If 𝐴 is contained in 𝐵, then (𝐶 ∖ 𝐵) is contained in (𝐶 ∖ 𝐴). Deduction form of sscon 4130. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))
Theorem	ssdifssd 4134	If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is also contained in 𝐵. Deduction form of ssdifss 4127. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵)
Theorem	ssdif2d 4135	If 𝐴 is contained in 𝐵 and 𝐶 is contained in 𝐷, then (𝐴 ∖ 𝐷) is contained in (𝐵 ∖ 𝐶). Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ (𝐵 ∖ 𝐶))
Theorem	raldifb 4136	Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018.)
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∉ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ (𝐴 ∖ 𝐵)𝜑)
Theorem	rexdifi 4137	Restricted existential quantification over a difference. (Contributed by AV, 25-Oct-2023.)
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝜑) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)𝜑)
Theorem	complss 4138	Complementation reverses inclusion. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 19-Mar-2021.)
⊢ (𝐴 ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ (V ∖ 𝐴))
Theorem	compleq 4139	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 4140	Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.)
⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))
Theorem	elunnel1 4141	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 4142	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 4143*	Inference from membership to union. (Contributed by NM, 21-Jun-1993.)
⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∪ 𝐵) = 𝐶
Theorem	unidm 4144	Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 21-Jun-1993.)
⊢ (𝐴 ∪ 𝐴) = 𝐴
Theorem	uncom 4145	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 4146	If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom 4146 was automatically derived from equncomVD 44118 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.)
⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵))
Theorem	equncomi 4147	Inference form of equncom 4146. equncomi 4147 was automatically derived from equncomiVD 44119 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.)
⊢ 𝐴 = (𝐵 ∪ 𝐶)    ⇒   ⊢ 𝐴 = (𝐶 ∪ 𝐵)
Theorem	uneq1 4148	Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993.)
⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
Theorem	uneq2 4149	Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
Theorem	uneq12 4150	Equality theorem for the union of two classes. (Contributed by NM, 29-Mar-1998.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
Theorem	uneq1i 4151	Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)
Theorem	uneq2i 4152	Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)
Theorem	uneq12i 4153	Equality inference for the union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)
Theorem	uneq1d 4154	Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
Theorem	uneq2d 4155	Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
Theorem	uneq12d 4156	Equality deduction for the union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
Theorem	nfun 4157	Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)
Theorem	unass 4158	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 4159	A rearrangement of union. (Contributed by NM, 12-Aug-2004.)
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (𝐴 ∪ 𝐶))
Theorem	un23 4160	A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ 𝐵)
Theorem	un4 4161	A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∪ (𝐶 ∪ 𝐷)) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐷))
Theorem	unundi 4162	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∪ (𝐴 ∪ 𝐶))
Theorem	unundir 4163	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐶))
Theorem	ssun1 4164	Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
Theorem	ssun2 4165	Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)
Theorem	ssun3 4166	Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐵 ∪ 𝐶))
Theorem	ssun4 4167	Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐶 ∪ 𝐵))
Theorem	elun1 4168	Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))
Theorem	elun2 4169	Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))
Theorem	elunant 4170	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 4171	Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶))
Theorem	ssequn1 4172	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 4173	Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∪ 𝐴) ⊆ (𝐶 ∪ 𝐵))
Theorem	unss12 4174	Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷))
Theorem	ssequn2 4175	A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
Theorem	unss 4176	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 4177	An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.)
⊢ 𝐴 ⊆ 𝐶    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶
Theorem	unssd 4178	A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)
Theorem	unssad 4179	If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4176. Partial converse of unssd 4178. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	unssbd 4180	If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 4176. Partial converse of unssd 4178. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
Theorem	ssun 4181	A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶) → 𝐴 ⊆ (𝐵 ∪ 𝐶))
Theorem	rexun 4182	Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑))
Theorem	ralunb 4183	Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	ralun 4184	Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑)
2.1.13.3  The intersection of two classes
Theorem	elini 4185	Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐴 ∈ 𝐶    ⇒   ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶)
Theorem	elind 4186	Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))
Theorem	elinel1 4187	Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵)
Theorem	elinel2 4188	Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)
Theorem	elin2 4189	Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑋 = (𝐵 ∩ 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
Theorem	elin1d 4190	Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐴)
Theorem	elin2d 4191	Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	elin3 4192	Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑋 = ((𝐵 ∩ 𝐶) ∩ 𝐷)    ⇒   ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷))
Theorem	incom 4193	Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.) (Proof shortened by SN, 12-Dec-2023.)
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
Theorem	ineqcom 4194	Two ways of expressing that two classes have a given intersection. This is often used when that given intersection is the empty set, in which case the statement displays two ways of expressing that two classes are disjoint (when 𝐶 = ∅: ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐵 ∩ 𝐴) = ∅)). (Contributed by Peter Mazsa, 22-Mar-2017.)
⊢ ((𝐴 ∩ 𝐵) = 𝐶 ↔ (𝐵 ∩ 𝐴) = 𝐶)
Theorem	ineqcomi 4195	Two ways of expressing that two classes have a given intersection. Inference form of ineqcom 4194. Disjointness inference when 𝐶 = ∅. (Contributed by Peter Mazsa, 26-Mar-2017.) (Proof shortened by SN, 20-Sep-2024.)
⊢ (𝐴 ∩ 𝐵) = 𝐶    ⇒   ⊢ (𝐵 ∩ 𝐴) = 𝐶
Theorem	ineqri 4196*	Inference from membership to intersection. (Contributed by NM, 21-Jun-1993.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∩ 𝐵) = 𝐶
Theorem	ineq1 4197	Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.) (Proof shortened by SN, 20-Sep-2023.)
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
Theorem	ineq2 4198	Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))
Theorem	ineq12 4199	Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
Theorem	ineq1i 4200	Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)