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	inindi 4201	Intersection distributes over itself. (Contributed by NM, 6-May-1994.)
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = ((𝐴 ∩ 𝐵) ∩ (𝐴 ∩ 𝐶))
Theorem	inindir 4202	Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶))
Theorem	inss1 4203	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 4204	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 4205	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 4206	An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.)
⊢ 𝐴 ⊆ 𝐵    &   ⊢ 𝐴 ⊆ 𝐶    ⇒   ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶)
Theorem	ssind 4207	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 4208	Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
Theorem	sslin 4209	Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵))
Theorem	ssrind 4210	Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
Theorem	ss2in 4211	Intersection of subclasses. (Contributed by NM, 5-May-2000.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))
Theorem	ssinss1 4212	Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	ssinss1d 4213	Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	inss 4214	Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.)
⊢ ((𝐴 ⊆ 𝐶 ∨ 𝐵 ⊆ 𝐶) → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	ralin 4215	Restricted universal quantification over intersection. (Contributed by Peter Mazsa, 8-Sep-2023.)
⊢ (∀𝑥 ∈ (𝐴 ∩ 𝐵)𝜑 ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑))
Theorem	rexin 4216	Restricted existential quantification over intersection. (Contributed by Peter Mazsa, 17-Dec-2018.)
⊢ (∃𝑥 ∈ (𝐴 ∩ 𝐵)𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ 𝜑))
Theorem	dfss7 4217*	Alternate definition of subclass relationship. (Contributed by AV, 1-Aug-2022.)
⊢ (𝐵 ⊆ 𝐴 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = 𝐵)
2.1.13.4  The symmetric difference of two classes
Syntax	csymdif 4218	Declare the syntax for symmetric difference.
class (𝐴 △ 𝐵)
Definition	df-symdif 4219	Define the symmetric difference of two classes. Alternate definitions are dfsymdif2 4227, dfsymdif3 4272 and dfsymdif4 4225. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 △ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))
Theorem	symdifcom 4220	Symmetric difference commutes. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 △ 𝐵) = (𝐵 △ 𝐴)
Theorem	symdifeq1 4221	Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 = 𝐵 → (𝐴 △ 𝐶) = (𝐵 △ 𝐶))
Theorem	symdifeq2 4222	Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 = 𝐵 → (𝐶 △ 𝐴) = (𝐶 △ 𝐵))
Theorem	nfsymdif 4223	Hypothesis builder for symmetric difference. (Contributed by Scott Fenton, 19-Feb-2013.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 △ 𝐵)
Theorem	elsymdif 4224	Membership in a symmetric difference. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ∈ (𝐵 △ 𝐶) ↔ ¬ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
Theorem	dfsymdif4 4225*	Alternate definition of the symmetric difference. (Contributed by NM, 17-Aug-2004.) (Revised by AV, 17-Aug-2022.)
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)}
Theorem	elsymdifxor 4226	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 4227*	Alternate definition of the symmetric difference. (Contributed by BJ, 30-Apr-2020.)
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵)}
Theorem	symdifass 4228	Symmetric difference is associative. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by BJ, 7-Sep-2022.)
⊢ ((𝐴 △ 𝐵) △ 𝐶) = (𝐴 △ (𝐵 △ 𝐶))
Theorem	difsssymdif 4229	The symmetric difference contains one of the differences. (Proposed by BJ, 18-Aug-2022.) (Contributed by AV, 19-Aug-2022.)
⊢ (𝐴 ∖ 𝐵) ⊆ (𝐴 △ 𝐵)
Theorem	difsymssdifssd 4230	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 4231	Absorption law for union. (Contributed by NM, 16-Apr-2006.)
⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴
Theorem	inabs 4232	Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
⊢ (𝐴 ∩ (𝐴 ∪ 𝐵)) = 𝐴
Theorem	nssinpss 4233	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 4234	Negation of subclass expressed in terms of proper subclass and union. (Contributed by NM, 15-Sep-2004.)
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ 𝐵 ⊊ (𝐴 ∪ 𝐵))
Theorem	dfss4 4235	Subclass defined in terms of class difference. See comments under dfun2 4236. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴)
Theorem	dfun2 4236	An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 4237 and dfss4 4235 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 4237	An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 4236. Another version is given by dfin4 4244. (Contributed by NM, 10-Jun-2004.)
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵))
Theorem	difin 4238	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 4239	Implication of a class difference with a subclass. (Contributed by AV, 3-Jan-2022.)
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 = (𝑉 ∖ 𝐴)) → 𝐴 = (𝑉 ∖ 𝐵))
Theorem	ssdifsym 4240	Symmetric class differences for subclasses. (Contributed by AV, 3-Jan-2022.)
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 ⊆ 𝑉) → (𝐵 = (𝑉 ∖ 𝐴) ↔ 𝐴 = (𝑉 ∖ 𝐵)))
Theorem	dfss5 4241*	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 4242	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 4243	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 4244	Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.)
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵))
Theorem	invdif 4245	Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
Theorem	indif 4246	Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∖ 𝐵)
Theorem	indif2 4247	Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
Theorem	indif1 4248	Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
Theorem	indifcom 4249	Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = (𝐵 ∩ (𝐴 ∖ 𝐶))
Theorem	indi 4250	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 4251	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 4252	Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶))
Theorem	undir 4253	Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
⊢ ((𝐴 ∩ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∩ (𝐵 ∪ 𝐶))
Theorem	unineq 4254	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 4255	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 4256	Distributive law for class difference. Theorem 39 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∩ (𝐴 ∖ 𝐶))
Theorem	difundir 4257	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
Theorem	difindi 4258	Distributive law for class difference. Theorem 40 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶))
Theorem	difindir 4259	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (𝐵 ∖ 𝐶))
Theorem	indifdi 4260	Distribute intersection over difference. (Contributed by BTernaryTau, 14-Aug-2024.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ (𝐴 ∩ 𝐶))
Theorem	indifdir 4261	Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.) (Revised by BTernaryTau, 14-Aug-2024.)
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶))
Theorem	difdif2 4262	Class difference by a class difference. (Contributed by Thierry Arnoux, 18-Dec-2017.)
⊢ (𝐴 ∖ (𝐵 ∖ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∩ 𝐶))
Theorem	undm 4263	De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.)
⊢ (V ∖ (𝐴 ∪ 𝐵)) = ((V ∖ 𝐴) ∩ (V ∖ 𝐵))
Theorem	indm 4264	De Morgan's law for intersection. Theorem 5.2(13') of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.)
⊢ (V ∖ (𝐴 ∩ 𝐵)) = ((V ∖ 𝐴) ∪ (V ∖ 𝐵))
Theorem	difun1 4265	A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.)
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∖ 𝐶)
Theorem	undif3 4266	An equality involving class union and class difference. The first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 17-Apr-2012.) (Proof shortened by JJ, 13-Jul-2021.)
⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴))
Theorem	difin2 4267	Represent a class difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = ((𝐶 ∖ 𝐵) ∩ 𝐴))
Theorem	dif32 4268	Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.)
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵)
Theorem	difabs 4269	Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009.)
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)
Theorem	sscon34b 4270	Relative complementation reverses inclusion of subclasses. Relativized version of complss 4117. (Contributed by RP, 3-Jun-2021.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)))
Theorem	rcompleq 4271	Two subclasses are equal if and only if their relative complements are equal. Relativized version of compleq 4118. (Contributed by RP, 10-Jun-2021.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 = 𝐵 ↔ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)))
Theorem	dfsymdif3 4272	Alternate definition of the symmetric difference, given in Example 4.1 of [Stoll] p. 262 (the original definition corresponds to [Stoll] p. 13). (Contributed by NM, 17-Aug-2004.) (Revised by BJ, 30-Apr-2020.)
⊢ (𝐴 △ 𝐵) = ((𝐴 ∪ 𝐵) ∖ (𝐴 ∩ 𝐵))
2.1.13.6  Class abstractions with difference, union, and intersection of two classes
Theorem	unabw 4273*	Union of two class abstractions. Version of unab 4274 using implicit substitution, which does not require ax-8 2111, ax-10 2142, ax-12 2178. (Contributed by GG, 15-Oct-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    ⇒   ⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑦 ∣ (𝜒 ∨ 𝜃)}
Theorem	unab 4274	Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)}
Theorem	inab 4275	Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∩ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ 𝜓)}
Theorem	difab 4276	Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∖ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ ¬ 𝜓)}
Theorem	abanssl 4277	A class abstraction with a conjunction is a subset of the class abstraction with the left conjunct only. (Contributed by AV, 7-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.)
⊢ {𝑓 ∣ (𝜑 ∧ 𝜓)} ⊆ {𝑓 ∣ 𝜑}
Theorem	abanssr 4278	A class abstraction with a conjunction is a subset of the class abstraction with the right conjunct only. (Contributed by AV, 7-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.)
⊢ {𝑓 ∣ (𝜑 ∧ 𝜓)} ⊆ {𝑓 ∣ 𝜓}
Theorem	notabw 4279*	A class abstraction defined by a negation. Version of notab 4280 using implicit substitution, which does not require ax-10 2142, ax-12 2178. (Contributed by GG, 15-Oct-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑦 ∣ 𝜓})
Theorem	notab 4280	A class abstraction defined by a negation. (Contributed by FL, 18-Sep-2010.)
⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑥 ∣ 𝜑})
Theorem	unrab 4281	Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)}
Theorem	inrab 4282	Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	inrab2 4283*	Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑}
Theorem	difrab 4284	Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)}
Theorem	dfrab3 4285*	Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑})
Theorem	dfrab2 4286*	Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.) (Proof shortened by BJ, 22-Apr-2019.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴)
Theorem	rabdif 4287*	Move difference in and out of a restricted class abstraction. (Contributed by Steven Nguyen, 6-Jun-2023.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ 𝐵) = {𝑥 ∈ (𝐴 ∖ 𝐵) ∣ 𝜑}
Theorem	notrab 4288*	Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}
Theorem	dfrab3ss 4289*	Restricted class abstraction with a common superset. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 8-Nov-2015.)
⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}))
Theorem	rabun2 4290	Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015.)
⊢ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝜑} = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜑})
2.1.13.7  Restricted uniqueness with difference, union, and intersection
Theorem	reuun2 4291	Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Wolf Lammen, 15-May-2025.)
⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑))
Theorem	reuss2 4292*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005.)
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuss 4293*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuun1 4294*	Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.)
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reupick 4295*	Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.)
⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	reupick3 4296*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.)
⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓))
Theorem	reupick2 4297*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 15-Dec-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ (((∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) ∧ ∃𝑥 ∈ 𝐴 𝜓 ∧ ∃!𝑥 ∈ 𝐴 𝜑) ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝜓))
Theorem	euelss 4298*	Transfer uniqueness of an element to a smaller subclass. (Contributed by AV, 14-Apr-2020.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴 ∧ ∃!𝑥 𝑥 ∈ 𝐵) → ∃!𝑥 𝑥 ∈ 𝐴)
2.1.14  The empty set
Syntax	c0 4299	Extend class notation to include the empty set.
class ∅
Definition	df-nul 4300	Define the empty set. More precisely, we should write "empty class". It will be posited in ax-nul 5264 that an empty set exists. Then, by uniqueness among classes (eq0 4316, as opposed to the weaker uniqueness among sets, nulmo 2707), it will follow that ∅ is indeed a set (0ex 5265). Special case of Exercise 4.10(o) of [Mendelson] p. 231. For a more traditional definition, but requiring a dummy variable, see dfnul2 4302. (Contributed by NM, 17-Jun-1993.) Clarify that at this point, it is not established that it is a set. (Revised by BJ, 22-Sep-2022.)
⊢ ∅ = (V ∖ V)