P. 43 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4201-4300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	unssd 4201	A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)
Theorem	unssad 4202	If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4199. Partial converse of unssd 4201. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	unssbd 4203	If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 4199. Partial converse of unssd 4201. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
Theorem	ssun 4204	A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶) → 𝐴 ⊆ (𝐵 ∪ 𝐶))
Theorem	rexun 4205	Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑))
Theorem	ralunb 4206	Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	ralun 4207	Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑)
2.1.13.3  The intersection of two classes
Theorem	elini 4208	Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐴 ∈ 𝐶    ⇒   ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶)
Theorem	elind 4209	Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))
Theorem	elinel1 4210	Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵)
Theorem	elinel2 4211	Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)
Theorem	elin2 4212	Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑋 = (𝐵 ∩ 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
Theorem	elin1d 4213	Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐴)
Theorem	elin2d 4214	Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	elin3 4215	Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑋 = ((𝐵 ∩ 𝐶) ∩ 𝐷)    ⇒   ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷))
Theorem	incom 4216	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 4217	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 4218	Two ways of expressing that two classes have a given intersection. Inference form of ineqcom 4217. Disjointness inference when 𝐶 = ∅. (Contributed by Peter Mazsa, 26-Mar-2017.) (Proof shortened by SN, 20-Sep-2024.)
⊢ (𝐴 ∩ 𝐵) = 𝐶    ⇒   ⊢ (𝐵 ∩ 𝐴) = 𝐶
Theorem	ineqri 4219*	Inference from membership to intersection. (Contributed by NM, 21-Jun-1993.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∩ 𝐵) = 𝐶
Theorem	ineq1 4220	Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.) (Proof shortened by SN, 20-Sep-2023.)
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
Theorem	ineq2 4221	Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))
Theorem	ineq12 4222	Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
Theorem	ineq1i 4223	Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)
Theorem	ineq2i 4224	Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)
Theorem	ineq12i 4225	Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)
Theorem	ineq1d 4226	Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
Theorem	ineq2d 4227	Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))
Theorem	ineq12d 4228	Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
Theorem	ineqan12d 4229	Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
Theorem	sseqin2 4230	A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)
Theorem	nfin 4231	Bound-variable hypothesis builder for the intersection 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	nfinOLD 4232	Obsolete version of nfin 4231 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	rabbi2dva 4233*	Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓})
Theorem	inidm 4234	Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ∩ 𝐴) = 𝐴
Theorem	inass 4235	Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶))
Theorem	in12 4236	A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.)
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐵 ∩ (𝐴 ∩ 𝐶))
Theorem	in32 4237	A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ 𝐵)
Theorem	in13 4238	A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐶 ∩ (𝐵 ∩ 𝐴))
Theorem	in31 4239	A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐵) ∩ 𝐴)
Theorem	inrot 4240	Rotate the intersection of 3 classes. (Contributed by NM, 27-Aug-2012.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐴) ∩ 𝐵)
Theorem	in4 4241	Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001.)
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐷)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐷))
Theorem	inindi 4242	Intersection distributes over itself. (Contributed by NM, 6-May-1994.)
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = ((𝐴 ∩ 𝐵) ∩ (𝐴 ∩ 𝐶))
Theorem	inindir 4243	Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶))
Theorem	inss1 4244	The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
Theorem	inss2 4245	The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵
Theorem	ssin 4246	Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26. (Contributed by NM, 15-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶))
Theorem	ssini 4247	An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐴 ⊆ 𝐶    ⇒   ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶)
Theorem	ssind 4248	A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶))
Theorem	ssrin 4249	Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
Theorem	sslin 4250	Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵))
Theorem	ssrind 4251	Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
Theorem	ss2in 4252	Intersection of subclasses. (Contributed by NM, 5-May-2000.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))
Theorem	ssinss1 4253	Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	inss 4254	Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.)
⊢ ((𝐴 ⊆ 𝐶 ∨ 𝐵 ⊆ 𝐶) → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	rexin 4255	Restricted existential quantification over intersection. (Contributed by Peter Mazsa, 17-Dec-2018.)
⊢ (∃𝑥 ∈ (𝐴 ∩ 𝐵)𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ 𝜑))
Theorem	dfss7 4256*	Alternate definition of subclass relationship. (Contributed by AV, 1-Aug-2022.)
⊢ (𝐵 ⊆ 𝐴 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = 𝐵)
2.1.13.4  The symmetric difference of two classes
Syntax	csymdif 4257	Declare the syntax for symmetric difference.
class (𝐴 △ 𝐵)
Definition	df-symdif 4258	Define the symmetric difference of two classes. Alternate definitions are dfsymdif2 4266, dfsymdif3 4311 and dfsymdif4 4264. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 △ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))
Theorem	symdifcom 4259	Symmetric difference commutes. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 △ 𝐵) = (𝐵 △ 𝐴)
Theorem	symdifeq1 4260	Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 = 𝐵 → (𝐴 △ 𝐶) = (𝐵 △ 𝐶))
Theorem	symdifeq2 4261	Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 = 𝐵 → (𝐶 △ 𝐴) = (𝐶 △ 𝐵))
Theorem	nfsymdif 4262	Hypothesis builder for symmetric difference. (Contributed by Scott Fenton, 19-Feb-2013.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 △ 𝐵)
Theorem	elsymdif 4263	Membership in a symmetric difference. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ∈ (𝐵 △ 𝐶) ↔ ¬ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
Theorem	dfsymdif4 4264*	Alternate definition of the symmetric difference. (Contributed by NM, 17-Aug-2004.) (Revised by AV, 17-Aug-2022.)
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)}
Theorem	elsymdifxor 4265	Membership in a symmetric difference is an exclusive-or relationship. (Contributed by David A. Wheeler, 26-Apr-2020.) (Proof shortened by BJ, 13-Aug-2022.)
⊢ (𝐴 ∈ (𝐵 △ 𝐶) ↔ (𝐴 ∈ 𝐵 ⊻ 𝐴 ∈ 𝐶))
Theorem	dfsymdif2 4266*	Alternate definition of the symmetric difference. (Contributed by BJ, 30-Apr-2020.)
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵)}
Theorem	symdifass 4267	Symmetric difference is associative. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by BJ, 7-Sep-2022.)
⊢ ((𝐴 △ 𝐵) △ 𝐶) = (𝐴 △ (𝐵 △ 𝐶))
Theorem	difsssymdif 4268	The symmetric difference contains one of the differences. (Proposed by BJ, 18-Aug-2022.) (Contributed by AV, 19-Aug-2022.)
⊢ (𝐴 ∖ 𝐵) ⊆ (𝐴 △ 𝐵)
Theorem	difsymssdifssd 4269	If the symmetric difference is contained in 𝐶, so is one of the differences. (Contributed by AV, 17-Aug-2022.)
⊢ (𝜑 → (𝐴 △ 𝐵) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐶)
2.1.13.5  Combinations of difference, union, and intersection of two classes
Theorem	unabs 4270	Absorption law for union. (Contributed by NM, 16-Apr-2006.)
⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴
Theorem	inabs 4271	Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
⊢ (𝐴 ∩ (𝐴 ∪ 𝐵)) = 𝐴
Theorem	nssinpss 4272	Negation of subclass expressed in terms of intersection and proper subclass. (Contributed by NM, 30-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) ⊊ 𝐴)
Theorem	nsspssun 4273	Negation of subclass expressed in terms of proper subclass and union. (Contributed by NM, 15-Sep-2004.)
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ 𝐵 ⊊ (𝐴 ∪ 𝐵))
Theorem	dfss4 4274	Subclass defined in terms of class difference. See comments under dfun2 4275. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴)
Theorem	dfun2 4275	An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 4276 and dfss4 4274 it shows we can express union, intersection, and subset directly in terms of the single "primitive" operation ∖ (class difference). (Contributed by NM, 10-Jun-2004.)
⊢ (𝐴 ∪ 𝐵) = (V ∖ ((V ∖ 𝐴) ∖ 𝐵))
Theorem	dfin2 4276	An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 4275. Another version is given by dfin4 4283. (Contributed by NM, 10-Jun-2004.)
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵))
Theorem	difin 4277	Difference with intersection. Theorem 33 of [Suppes] p. 29. (Contributed by NM, 31-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵)
Theorem	ssdifim 4278	Implication of a class difference with a subclass. (Contributed by AV, 3-Jan-2022.)
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 = (𝑉 ∖ 𝐴)) → 𝐴 = (𝑉 ∖ 𝐵))
Theorem	ssdifsym 4279	Symmetric class differences for subclasses. (Contributed by AV, 3-Jan-2022.)
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 ⊆ 𝑉) → (𝐵 = (𝑉 ∖ 𝐴) ↔ 𝐴 = (𝑉 ∖ 𝐵)))
Theorem	dfss5 4280*	Alternate definition of subclass relationship: a class 𝐴 is a subclass of another class 𝐵 iff each element of 𝐴 is equal to an element of 𝐵. (Contributed by AV, 13-Nov-2020.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝑦)
Theorem	dfun3 4281	Union defined in terms of intersection (De Morgan's law). Definition of union in [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.)
⊢ (𝐴 ∪ 𝐵) = (V ∖ ((V ∖ 𝐴) ∩ (V ∖ 𝐵)))
Theorem	dfin3 4282	Intersection defined in terms of union (De Morgan's law). Similar to Exercise 4.10(n) of [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.)
⊢ (𝐴 ∩ 𝐵) = (V ∖ ((V ∖ 𝐴) ∪ (V ∖ 𝐵)))
Theorem	dfin4 4283	Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.)
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵))
Theorem	invdif 4284	Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
Theorem	indif 4285	Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∖ 𝐵)
Theorem	indif2 4286	Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
Theorem	indif1 4287	Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
Theorem	indifcom 4288	Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = (𝐵 ∩ (𝐴 ∖ 𝐶))
Theorem	indi 4289	Distributive law for intersection over union. Exercise 10 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶))
Theorem	undi 4290	Distributive law for union over intersection. Exercise 11 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ∪ (𝐵 ∩ 𝐶)) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ 𝐶))
Theorem	indir 4291	Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶))
Theorem	undir 4292	Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
⊢ ((𝐴 ∩ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∩ (𝐵 ∪ 𝐶))
Theorem	unineq 4293	Infer equality from equalities of union and intersection. Exercise 20 of [Enderton] p. 32 and its converse. (Contributed by NM, 10-Aug-2004.)
⊢ (((𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶) ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) ↔ 𝐴 = 𝐵)
Theorem	uneqin 4294	Equality of union and intersection implies equality of their arguments. (Contributed by NM, 16-Apr-2006.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) ↔ 𝐴 = 𝐵)
Theorem	difundi 4295	Distributive law for class difference. Theorem 39 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∩ (𝐴 ∖ 𝐶))
Theorem	difundir 4296	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
Theorem	difindi 4297	Distributive law for class difference. Theorem 40 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶))
Theorem	difindir 4298	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (𝐵 ∖ 𝐶))
Theorem	indifdi 4299	Distribute intersection over difference. (Contributed by BTernaryTau, 14-Aug-2024.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ (𝐴 ∩ 𝐶))
Theorem	indifdir 4300	Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.) (Revised by BTernaryTau, 14-Aug-2024.)
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶))