Type  Label  Description 
Statement 

Theorem  un12 3101 
A rearrangement of union. (Contributed by NM, 12Aug2004.)

⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (𝐴 ∪ 𝐶)) 

Theorem  un23 3102 
A rearrangement of union. (Contributed by NM, 12Aug2004.) (Proof
shortened by Andrew Salmon, 26Jun2011.)

⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ 𝐵) 

Theorem  un4 3103 
A rearrangement of the union of 4 classes. (Contributed by NM,
12Aug2004.)

⊢ ((𝐴 ∪ 𝐵) ∪ (𝐶 ∪ 𝐷)) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐷)) 

Theorem  unundi 3104 
Union distributes over itself. (Contributed by NM, 17Aug2004.)

⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∪ (𝐴 ∪ 𝐶)) 

Theorem  unundir 3105 
Union distributes over itself. (Contributed by NM, 17Aug2004.)

⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐶)) 

Theorem  ssun1 3106 
Subclass relationship for union of classes. Theorem 25 of [Suppes]
p. 27. (Contributed by NM, 5Aug1993.)

⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) 

Theorem  ssun2 3107 
Subclass relationship for union of classes. (Contributed by NM,
30Aug1993.)

⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴) 

Theorem  ssun3 3108 
Subclass law for union of classes. (Contributed by NM, 5Aug1993.)

⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐵 ∪ 𝐶)) 

Theorem  ssun4 3109 
Subclass law for union of classes. (Contributed by NM, 14Aug1994.)

⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐶 ∪ 𝐵)) 

Theorem  elun1 3110 
Membership law for union of classes. (Contributed by NM, 5Aug1993.)

⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶)) 

Theorem  elun2 3111 
Membership law for union of classes. (Contributed by NM, 30Aug1993.)

⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵)) 

Theorem  unss1 3112 
Subclass law for union of classes. (Contributed by NM, 14Oct1999.)
(Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶)) 

Theorem  ssequn1 3113 
A relationship between subclass and union. Theorem 26 of [Suppes]
p. 27. (Contributed by NM, 30Aug1993.) (Proof shortened by Andrew
Salmon, 26Jun2011.)

⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) 

Theorem  unss2 3114 
Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18.
(Contributed by NM, 14Oct1999.)

⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∪ 𝐴) ⊆ (𝐶 ∪ 𝐵)) 

Theorem  unss12 3115 
Subclass law for union of classes. (Contributed by NM, 2Jun2004.)

⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) 

Theorem  ssequn2 3116 
A relationship between subclass and union. (Contributed by NM,
13Jun1994.)

⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵) 

Theorem  unss 3117 
The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27
and its converse. (Contributed by NM, 11Jun2004.)

⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) 

Theorem  unssi 3118 
An inference showing the union of two subclasses is a subclass.
(Contributed by Raph Levien, 10Dec2002.)

⊢ 𝐴 ⊆ 𝐶
& ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶 

Theorem  unssd 3119 
A deduction showing the union of two subclasses is a subclass.
(Contributed by Jonathan BenNaim, 3Jun2011.)

⊢ (𝜑 → 𝐴 ⊆ 𝐶)
& ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) 

Theorem  unssad 3120 
If (𝐴
∪ 𝐵) is
contained in 𝐶, so is 𝐴. Oneway
deduction form of unss 3117. Partial converse of unssd 3119. (Contributed
by David Moews, 1May2017.)

⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) 

Theorem  unssbd 3121 
If (𝐴
∪ 𝐵) is
contained in 𝐶, so is 𝐵. Oneway
deduction form of unss 3117. Partial converse of unssd 3119. (Contributed
by David Moews, 1May2017.)

⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐶) 

Theorem  ssun 3122 
A condition that implies inclusion in the union of two classes.
(Contributed by NM, 23Nov2003.)

⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶) → 𝐴 ⊆ (𝐵 ∪ 𝐶)) 

Theorem  rexun 3123 
Restricted existential quantification over union. (Contributed by Jeff
Madsen, 5Jan2011.)

⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑)) 

Theorem  ralunb 3124 
Restricted quantification over a union. (Contributed by Scott Fenton,
12Apr2011.) (Proof shortened by Andrew Salmon, 29Jun2011.)

⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑)) 

Theorem  ralun 3125 
Restricted quantification over union. (Contributed by Jeff Madsen,
2Sep2009.)

⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑) 

2.1.13.3 The intersection of two
classes


Theorem  elin 3126 
Expansion of membership in an intersection of two classes. Theorem 12
of [Suppes] p. 25. (Contributed by NM,
29Apr1994.)

⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) 

Theorem  elin2 3127 
Membership in a class defined as an intersection. (Contributed by
Stefan O'Rear, 29Mar2015.)

⊢ 𝑋 = (𝐵 ∩ 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) 

Theorem  elin3 3128 
Membership in a class defined as a ternary intersection. (Contributed
by Stefan O'Rear, 29Mar2015.)

⊢ 𝑋 = ((𝐵 ∩ 𝐶) ∩ 𝐷) ⇒ ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷)) 

Theorem  incom 3129 
Commutative law for intersection of classes. Exercise 7 of
[TakeutiZaring] p. 17.
(Contributed by NM, 5Aug1993.)

⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) 

Theorem  ineqri 3130* 
Inference from membership to intersection. (Contributed by NM,
5Aug1993.)

⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ⇒ ⊢ (𝐴 ∩ 𝐵) = 𝐶 

Theorem  ineq1 3131 
Equality theorem for intersection of two classes. (Contributed by NM,
14Dec1993.)

⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) 

Theorem  ineq2 3132 
Equality theorem for intersection of two classes. (Contributed by NM,
26Dec1993.)

⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) 

Theorem  ineq12 3133 
Equality theorem for intersection of two classes. (Contributed by NM,
8May1994.)

⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) 

Theorem  ineq1i 3134 
Equality inference for intersection of two classes. (Contributed by NM,
26Dec1993.)

⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶) 

Theorem  ineq2i 3135 
Equality inference for intersection of two classes. (Contributed by NM,
26Dec1993.)

⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵) 

Theorem  ineq12i 3136 
Equality inference for intersection of two classes. (Contributed by
NM, 24Jun2004.) (Proof shortened by Eric Schmidt, 26Jan2007.)

⊢ 𝐴 = 𝐵
& ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷) 

Theorem  ineq1d 3137 
Equality deduction for intersection of two classes. (Contributed by NM,
10Apr1994.)

⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) 

Theorem  ineq2d 3138 
Equality deduction for intersection of two classes. (Contributed by NM,
10Apr1994.)

⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) 

Theorem  ineq12d 3139 
Equality deduction for intersection of two classes. (Contributed by
NM, 24Jun2004.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) 

Theorem  ineqan12d 3140 
Equality deduction for intersection of two classes. (Contributed by
NM, 7Feb2007.)

⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) 

Theorem  dfss1 3141 
A frequentlyused variant of subclass definition dfss 2931. (Contributed
by NM, 10Jan2015.)

⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) 

Theorem  dfss5 3142 
Another definition of subclasshood. Similar to dfss 2931, dfss 2932, and
dfss1 3141. (Contributed by David Moews, 1May2017.)

⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐵 ∩ 𝐴)) 

Theorem  nfin 3143 
Boundvariable hypothesis builder for the intersection of classes.
(Contributed by NM, 15Sep2003.) (Revised by Mario Carneiro,
14Oct2016.)

⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵) 

Theorem  csbing 3144 
Distribute proper substitution through an intersection relation.
(Contributed by Alan Sare, 22Jul2012.)

⊢ (𝐴 ∈ 𝐵 → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷)) 

Theorem  rabbi2dva 3145* 
Deduction from a wff to a restricted class abstraction. (Contributed by
NM, 14Jan2014.)

⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓}) 

Theorem  inidm 3146 
Idempotent law for intersection of classes. Theorem 15 of [Suppes]
p. 26. (Contributed by NM, 5Aug1993.)

⊢ (𝐴 ∩ 𝐴) = 𝐴 

Theorem  inass 3147 
Associative law for intersection of classes. Exercise 9 of
[TakeutiZaring] p. 17.
(Contributed by NM, 3May1994.)

⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶)) 

Theorem  in12 3148 
A rearrangement of intersection. (Contributed by NM, 21Apr2001.)

⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐵 ∩ (𝐴 ∩ 𝐶)) 

Theorem  in32 3149 
A rearrangement of intersection. (Contributed by NM, 21Apr2001.)
(Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ 𝐵) 

Theorem  in13 3150 
A rearrangement of intersection. (Contributed by NM, 27Aug2012.)

⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐶 ∩ (𝐵 ∩ 𝐴)) 

Theorem  in31 3151 
A rearrangement of intersection. (Contributed by NM, 27Aug2012.)

⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐵) ∩ 𝐴) 

Theorem  inrot 3152 
Rotate the intersection of 3 classes. (Contributed by NM,
27Aug2012.)

⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐴) ∩ 𝐵) 

Theorem  in4 3153 
Rearrangement of intersection of 4 classes. (Contributed by NM,
21Apr2001.)

⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐷)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐷)) 

Theorem  inindi 3154 
Intersection distributes over itself. (Contributed by NM, 6May1994.)

⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = ((𝐴 ∩ 𝐵) ∩ (𝐴 ∩ 𝐶)) 

Theorem  inindir 3155 
Intersection distributes over itself. (Contributed by NM,
17Aug2004.)

⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶)) 

Theorem  sseqin2 3156 
A relationship between subclass and intersection. Similar to Exercise 9
of [TakeutiZaring] p. 18.
(Contributed by NM, 17May1994.)

⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) 

Theorem  inss1 3157 
The intersection of two classes is a subset of one of them. Part of
Exercise 12 of [TakeutiZaring] p.
18. (Contributed by NM,
27Apr1994.)

⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 

Theorem  inss2 3158 
The intersection of two classes is a subset of one of them. Part of
Exercise 12 of [TakeutiZaring] p.
18. (Contributed by NM,
27Apr1994.)

⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 

Theorem  ssin 3159 
Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26.
(Contributed by NM, 15Jun2004.) (Proof shortened by Andrew Salmon,
26Jun2011.)

⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶)) 

Theorem  ssini 3160 
An inference showing that a subclass of two classes is a subclass of
their intersection. (Contributed by NM, 24Nov2003.)

⊢ 𝐴 ⊆ 𝐵
& ⊢ 𝐴 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶) 

Theorem  ssind 3161 
A deduction showing that a subclass of two classes is a subclass of
their intersection. (Contributed by Jonathan BenNaim, 3Jun2011.)

⊢ (𝜑 → 𝐴 ⊆ 𝐵)
& ⊢ (𝜑 → 𝐴 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶)) 

Theorem  ssrin 3162 
Add right intersection to subclass relation. (Contributed by NM,
16Aug1994.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) 

Theorem  sslin 3163 
Add left intersection to subclass relation. (Contributed by NM,
19Oct1999.)

⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵)) 

Theorem  ss2in 3164 
Intersection of subclasses. (Contributed by NM, 5May2000.)

⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) 

Theorem  ssinss1 3165 
Intersection preserves subclass relationship. (Contributed by NM,
14Sep1999.)

⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶) 

Theorem  inss 3166 
Inclusion of an intersection of two classes. (Contributed by NM,
30Oct2014.)

⊢ ((𝐴 ⊆ 𝐶 ∨ 𝐵 ⊆ 𝐶) → (𝐴 ∩ 𝐵) ⊆ 𝐶) 

2.1.13.4 Combinations of difference, union, and
intersection of two classes


Theorem  unabs 3167 
Absorption law for union. (Contributed by NM, 16Apr2006.)

⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴 

Theorem  inabs 3168 
Absorption law for intersection. (Contributed by NM, 16Apr2006.)

⊢ (𝐴 ∩ (𝐴 ∪ 𝐵)) = 𝐴 

Theorem  nssinpss 3169 
Negation of subclass expressed in terms of intersection and proper
subclass. (Contributed by NM, 30Jun2004.) (Proof shortened by Andrew
Salmon, 26Jun2011.)

⊢ (¬ 𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) ⊊ 𝐴) 

Theorem  nsspssun 3170 
Negation of subclass expressed in terms of proper subclass and union.
(Contributed by NM, 15Sep2004.)

⊢ (¬ 𝐴 ⊆ 𝐵 ↔ 𝐵 ⊊ (𝐴 ∪ 𝐵)) 

Theorem  ssddif 3171 
Double complement and subset. Similar to ddifss 3175 but inside a class
𝐵 instead of the universal class V. In classical logic the
subset operation on the right hand side could be an equality (that is,
𝐴
⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴). (Contributed by Jim Kingdon,
24Jul2018.)

⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ (𝐵 ∖ (𝐵 ∖ 𝐴))) 

Theorem  unssdif 3172 
Union of two classes and class difference. In classical logic this
would be an equality. (Contributed by Jim Kingdon, 24Jul2018.)

⊢ (𝐴 ∪ 𝐵) ⊆ (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) 

Theorem  inssdif 3173 
Intersection of two classes and class difference. In classical logic
this would be an equality. (Contributed by Jim Kingdon,
24Jul2018.)

⊢ (𝐴 ∩ 𝐵) ⊆ (𝐴 ∖ (V ∖ 𝐵)) 

Theorem  difin 3174 
Difference with intersection. Theorem 33 of [Suppes] p. 29.
(Contributed by NM, 31Mar1998.) (Proof shortened by Andrew Salmon,
26Jun2011.)

⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵) 

Theorem  ddifss 3175 
Double complement under universal class. In classical logic (or given an
additional hypothesis, as in ddifnel 3075), this is equality rather than
subset. (Contributed by Jim Kingdon, 24Jul2018.)

⊢ 𝐴 ⊆ (V ∖ (V ∖ 𝐴)) 

Theorem  unssin 3176 
Union as a subset of class complement and intersection (De Morgan's
law). One direction of the definition of union in [Mendelson] p. 231.
This would be an equality, rather than subset, in classical logic.
(Contributed by Jim Kingdon, 25Jul2018.)

⊢ (𝐴 ∪ 𝐵) ⊆ (V ∖ ((V ∖ 𝐴) ∩ (V ∖ 𝐵))) 

Theorem  inssun 3177 
Intersection in terms of class difference and union (De Morgan's law).
Similar to Exercise 4.10(n) of [Mendelson] p. 231. This would be an
equality, rather than subset, in classical logic. (Contributed by Jim
Kingdon, 25Jul2018.)

⊢ (𝐴 ∩ 𝐵) ⊆ (V ∖ ((V ∖ 𝐴) ∪ (V ∖ 𝐵))) 

Theorem  inssddif 3178 
Intersection of two classes and class difference. In classical logic,
such as Exercise 4.10(q) of [Mendelson]
p. 231, this is an equality rather
than subset. (Contributed by Jim Kingdon, 26Jul2018.)

⊢ (𝐴 ∩ 𝐵) ⊆ (𝐴 ∖ (𝐴 ∖ 𝐵)) 

Theorem  invdif 3179 
Intersection with universal complement. Remark in [Stoll] p. 20.
(Contributed by NM, 17Aug2004.)

⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) 

Theorem  indif 3180 
Intersection with class difference. Theorem 34 of [Suppes] p. 29.
(Contributed by NM, 17Aug2004.)

⊢ (𝐴 ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∖ 𝐵) 

Theorem  indif2 3181 
Bring an intersection in and out of a class difference. (Contributed by
Jeff Hankins, 15Jul2009.)

⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶) 

Theorem  indif1 3182 
Bring an intersection in and out of a class difference. (Contributed by
Mario Carneiro, 15May2015.)

⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶) 

Theorem  indifcom 3183 
Commutation law for intersection and difference. (Contributed by Scott
Fenton, 18Feb2013.)

⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = (𝐵 ∩ (𝐴 ∖ 𝐶)) 

Theorem  indi 3184 
Distributive law for intersection over union. Exercise 10 of
[TakeutiZaring] p. 17.
(Contributed by NM, 30Sep2002.) (Proof
shortened by Andrew Salmon, 26Jun2011.)

⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)) 

Theorem  undi 3185 
Distributive law for union over intersection. Exercise 11 of
[TakeutiZaring] p. 17.
(Contributed by NM, 30Sep2002.) (Proof
shortened by Andrew Salmon, 26Jun2011.)

⊢ (𝐴 ∪ (𝐵 ∩ 𝐶)) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ 𝐶)) 

Theorem  indir 3186 
Distributive law for intersection over union. Theorem 28 of [Suppes]
p. 27. (Contributed by NM, 30Sep2002.)

⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) 

Theorem  undir 3187 
Distributive law for union over intersection. Theorem 29 of [Suppes]
p. 27. (Contributed by NM, 30Sep2002.)

⊢ ((𝐴 ∩ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∩ (𝐵 ∪ 𝐶)) 

Theorem  uneqin 3188 
Equality of union and intersection implies equality of their arguments.
(Contributed by NM, 16Apr2006.) (Proof shortened by Andrew Salmon,
26Jun2011.)

⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) ↔ 𝐴 = 𝐵) 

Theorem  difundi 3189 
Distributive law for class difference. Theorem 39 of [Suppes] p. 29.
(Contributed by NM, 17Aug2004.)

⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∩ (𝐴 ∖ 𝐶)) 

Theorem  difundir 3190 
Distributive law for class difference. (Contributed by NM,
17Aug2004.)

⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) 

Theorem  difindiss 3191 
Distributive law for class difference. In classical logic, for example,
theorem 40 of [Suppes] p. 29, this is an
equality instead of subset.
(Contributed by Jim Kingdon, 26Jul2018.)

⊢ ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) ⊆ (𝐴 ∖ (𝐵 ∩ 𝐶)) 

Theorem  difindir 3192 
Distributive law for class difference. (Contributed by NM,
17Aug2004.)

⊢ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (𝐵 ∖ 𝐶)) 

Theorem  indifdir 3193 
Distribute intersection over difference. (Contributed by Scott Fenton,
14Apr2011.)

⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶)) 

Theorem  difdif2ss 3194 
Set difference with a set difference. In classical logic this would be
equality rather than subset. (Contributed by Jim Kingdon,
27Jul2018.)

⊢ ((𝐴 ∖ 𝐵) ∪ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∖ (𝐵 ∖ 𝐶)) 

Theorem  undm 3195 
De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19.
(Contributed by NM, 18Aug2004.)

⊢ (V ∖ (𝐴 ∪ 𝐵)) = ((V ∖ 𝐴) ∩ (V ∖ 𝐵)) 

Theorem  indmss 3196 
De Morgan's law for intersection. In classical logic, this would be
equality rather than subset, as in Theorem 5.2(13') of [Stoll] p. 19.
(Contributed by Jim Kingdon, 27Jul2018.)

⊢ ((V ∖ 𝐴) ∪ (V ∖ 𝐵)) ⊆ (V ∖ (𝐴 ∩ 𝐵)) 

Theorem  difun1 3197 
A relationship involving double difference and union. (Contributed by NM,
29Aug2004.)

⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∖ 𝐶) 

Theorem  undif3ss 3198 
A subset relationship involving class union and class difference. In
classical logic, this would be equality rather than subset, as in the
first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by
Jim Kingdon, 28Jul2018.)

⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) ⊆ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) 

Theorem  difin2 3199 
Represent a set difference as an intersection with a larger difference.
(Contributed by Jeff Madsen, 2Sep2009.)

⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = ((𝐶 ∖ 𝐵) ∩ 𝐴)) 

Theorem  dif32 3200 
Swap second and third argument of double difference. (Contributed by NM,
18Aug2004.)

⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵) 