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	ssun3 4001	Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐵 ∪ 𝐶))
Theorem	ssun4 4002	Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐶 ∪ 𝐵))
Theorem	elun1 4003	Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))
Theorem	elun2 4004	Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))
Theorem	unss1 4005	Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶))
Theorem	ssequn1 4006	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 4007	Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∪ 𝐴) ⊆ (𝐶 ∪ 𝐵))
Theorem	unss12 4008	Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷))
Theorem	ssequn2 4009	A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
Theorem	unss 4010	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 4011	An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.)
⊢ 𝐴 ⊆ 𝐶    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶
Theorem	unssd 4012	A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)
Theorem	unssad 4013	If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4010. Partial converse of unssd 4012. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
Theorem	unssbd 4014	If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 4010. Partial converse of unssd 4012. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
Theorem	ssun 4015	A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶) → 𝐴 ⊆ (𝐵 ∪ 𝐶))
Theorem	rexun 4016	Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑))
Theorem	ralunb 4017	Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	ralun 4018	Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑)
2.1.13.3  The intersection of two classes
Theorem	elin 4019	Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
Theorem	elini 4020	Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝐴 ∈ 𝐵    &   ⊢ 𝐴 ∈ 𝐶    ⇒   ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶)
Theorem	elind 4021	Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))
Theorem	elinel1 4022	Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵)
Theorem	elinel2 4023	Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)
Theorem	elin2 4024	Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑋 = (𝐵 ∩ 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
Theorem	elin1d 4025	Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐴)
Theorem	elin2d 4026	Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝐵)
Theorem	elin3 4027	Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑋 = ((𝐵 ∩ 𝐶) ∩ 𝐷)    ⇒   ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷))
Theorem	incom 4028	Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.)
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
Theorem	ineqri 4029*	Inference from membership to intersection. (Contributed by NM, 21-Jun-1993.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)    ⇒   ⊢ (𝐴 ∩ 𝐵) = 𝐶
Theorem	ineq1 4030	Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.)
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
Theorem	ineq2 4031	Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))
Theorem	ineq12 4032	Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
Theorem	ineq1i 4033	Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)
Theorem	ineq2i 4034	Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)
Theorem	ineq12i 4035	Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)
Theorem	ineq1d 4036	Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
Theorem	ineq2d 4037	Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))
Theorem	ineq12d 4038	Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
Theorem	ineqan12d 4039	Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
Theorem	sseqin2 4040	A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)
Theorem	nfin 4041	Bound-variable hypothesis builder for the intersection of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)
Theorem	rabbi2dva 4042*	Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓})
Theorem	inidm 4043	Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ∩ 𝐴) = 𝐴
Theorem	inass 4044	Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶))
Theorem	in12 4045	A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.)
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐵 ∩ (𝐴 ∩ 𝐶))
Theorem	in32 4046	A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ 𝐵)
Theorem	in13 4047	A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐶 ∩ (𝐵 ∩ 𝐴))
Theorem	in31 4048	A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐵) ∩ 𝐴)
Theorem	inrot 4049	Rotate the intersection of 3 classes. (Contributed by NM, 27-Aug-2012.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐴) ∩ 𝐵)
Theorem	in4 4050	Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001.)
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐷)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐷))
Theorem	inindi 4051	Intersection distributes over itself. (Contributed by NM, 6-May-1994.)
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = ((𝐴 ∩ 𝐵) ∩ (𝐴 ∩ 𝐶))
Theorem	inindir 4052	Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶))
Theorem	inss1 4053	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 4054	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 4055	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 4056	An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐴 ⊆ 𝐶    ⇒   ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶)
Theorem	ssind 4057	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 4058	Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
Theorem	sslin 4059	Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵))
Theorem	ssrind 4060	Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
Theorem	ss2in 4061	Intersection of subclasses. (Contributed by NM, 5-May-2000.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))
Theorem	ssinss1 4062	Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	inss 4063	Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.)
⊢ ((𝐴 ⊆ 𝐶 ∨ 𝐵 ⊆ 𝐶) → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	rexin 4064	Restricted existential quantification over intersection. (Contributed by Peter Mazsa, 17-Dec-2018.)
⊢ (∃𝑥 ∈ (𝐴 ∩ 𝐵)𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ 𝜑))
Theorem	dfss7 4065*	Alternate definition of subclass relationship. (Contributed by AV, 1-Aug-2022.)
⊢ (𝐵 ⊆ 𝐴 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = 𝐵)
2.1.13.4  The symmetric difference of two classes
Syntax	csymdif 4066	Declare the syntax for symmetric difference.
class (𝐴 △ 𝐵)
Definition	df-symdif 4067	Define the symmetric difference of two classes. Alternate definitions are dfsymdif2 4075, dfsymdif3 4119 and dfsymdif4 4073. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 △ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))
Theorem	symdifcom 4068	Symmetric difference commutes. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 △ 𝐵) = (𝐵 △ 𝐴)
Theorem	symdifeq1 4069	Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 = 𝐵 → (𝐴 △ 𝐶) = (𝐵 △ 𝐶))
Theorem	symdifeq2 4070	Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 = 𝐵 → (𝐶 △ 𝐴) = (𝐶 △ 𝐵))
Theorem	nfsymdif 4071	Hypothesis builder for symmetric difference. (Contributed by Scott Fenton, 19-Feb-2013.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 △ 𝐵)
Theorem	elsymdif 4072	Membership in a symmetric difference. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ∈ (𝐵 △ 𝐶) ↔ ¬ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
Theorem	dfsymdif4 4073*	Alternate definition of the symmetric difference. (Contributed by NM, 17-Aug-2004.) (Revised by AV, 17-Aug-2022.)
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)}
Theorem	elsymdifxor 4074	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 4075*	Alternate definition of the symmetric difference. (Contributed by BJ, 30-Apr-2020.)
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵)}
Theorem	symdifass 4076	Symmetric difference is associative. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by BJ, 7-Sep-2022.)
⊢ ((𝐴 △ 𝐵) △ 𝐶) = (𝐴 △ (𝐵 △ 𝐶))
Theorem	symdifassOLD 4077	Obsolete proof of symdifass 4076 as of 7-Sep-2022. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 △ (𝐵 △ 𝐶)) = ((𝐴 △ 𝐵) △ 𝐶)
Theorem	difsssymdif 4078	The symmetric difference contains one of the differences. (Proposed by BJ, 18-Aug-2022.) (Contributed by AV, 19-Aug-2022.)
⊢ (𝐴 ∖ 𝐵) ⊆ (𝐴 △ 𝐵)
Theorem	difsymssdifssd 4079	If the symmetric difference is contained in 𝐶, so is one of the differences. (Contributed by AV, 17-Aug-2022.)
⊢ (𝜑 → (𝐴 △ 𝐵) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐶)
Theorem	symdif2OLD 4080*	Obsolete version of dfsymdif4 4073 as of 18-Aug-2022. Two ways to express symmetric difference (df-symdif 4067). (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) = {𝑥 ∣ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)}
2.1.13.5  Combinations of difference, union, and intersection of two classes
Theorem	unabs 4081	Absorption law for union. (Contributed by NM, 16-Apr-2006.)
⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴
Theorem	inabs 4082	Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
⊢ (𝐴 ∩ (𝐴 ∪ 𝐵)) = 𝐴
Theorem	nssinpss 4083	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 4084	Negation of subclass expressed in terms of proper subclass and union. (Contributed by NM, 15-Sep-2004.)
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ 𝐵 ⊊ (𝐴 ∪ 𝐵))
Theorem	dfss4 4085	Subclass defined in terms of class difference. See comments under dfun2 4086. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴)
Theorem	dfun2 4086	An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 4087 and dfss4 4085 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 4087	An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 4086. Another version is given by dfin4 4094. (Contributed by NM, 10-Jun-2004.)
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵))
Theorem	difin 4088	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 4089	Implication of a class difference with a subclass. (Contributed by AV, 3-Jan-2022.)
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 = (𝑉 ∖ 𝐴)) → 𝐴 = (𝑉 ∖ 𝐵))
Theorem	ssdifsym 4090	Symmetric class differences for subclasses. (Contributed by AV, 3-Jan-2022.)
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 ⊆ 𝑉) → (𝐵 = (𝑉 ∖ 𝐴) ↔ 𝐴 = (𝑉 ∖ 𝐵)))
Theorem	dfss5 4091*	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 4092	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 4093	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 4094	Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.)
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵))
Theorem	invdif 4095	Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
Theorem	indif 4096	Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∖ 𝐵)
Theorem	indif2 4097	Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
Theorem	indif1 4098	Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
Theorem	indifcom 4099	Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = (𝐵 ∩ (𝐴 ∖ 𝐶))
Theorem	indi 4100	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.)
⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶))