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	ssinss1d 4201	Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	inss 4202	Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.)
⊢ ((𝐴 ⊆ 𝐶 ∨ 𝐵 ⊆ 𝐶) → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	ralin 4203	Restricted universal quantification over intersection. (Contributed by Peter Mazsa, 8-Sep-2023.)
⊢ (∀𝑥 ∈ (𝐴 ∩ 𝐵)𝜑 ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑))
Theorem	rexin 4204	Restricted existential quantification over intersection. (Contributed by Peter Mazsa, 17-Dec-2018.)
⊢ (∃𝑥 ∈ (𝐴 ∩ 𝐵)𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ 𝜑))
Theorem	dfss7 4205*	Alternate definition of subclass relationship. (Contributed by AV, 1-Aug-2022.)
⊢ (𝐵 ⊆ 𝐴 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = 𝐵)
2.1.13.4  The symmetric difference of two classes
Syntax	csymdif 4206	Declare the syntax for symmetric difference.
class (𝐴 △ 𝐵)
Definition	df-symdif 4207	Define the symmetric difference of two classes. Alternate definitions are dfsymdif2 4215, dfsymdif3 4260 and dfsymdif4 4213. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 △ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))
Theorem	symdifcom 4208	Symmetric difference commutes. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 △ 𝐵) = (𝐵 △ 𝐴)
Theorem	symdifeq1 4209	Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 = 𝐵 → (𝐴 △ 𝐶) = (𝐵 △ 𝐶))
Theorem	symdifeq2 4210	Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 = 𝐵 → (𝐶 △ 𝐴) = (𝐶 △ 𝐵))
Theorem	nfsymdif 4211	Hypothesis builder for symmetric difference. (Contributed by Scott Fenton, 19-Feb-2013.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 △ 𝐵)
Theorem	elsymdif 4212	Membership in a symmetric difference. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ∈ (𝐵 △ 𝐶) ↔ ¬ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
Theorem	dfsymdif4 4213*	Alternate definition of the symmetric difference. (Contributed by NM, 17-Aug-2004.) (Revised by AV, 17-Aug-2022.)
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)}
Theorem	elsymdifxor 4214	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 4215*	Alternate definition of the symmetric difference. (Contributed by BJ, 30-Apr-2020.)
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵)}
Theorem	symdifass 4216	Symmetric difference is associative. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by BJ, 7-Sep-2022.)
⊢ ((𝐴 △ 𝐵) △ 𝐶) = (𝐴 △ (𝐵 △ 𝐶))
Theorem	difsssymdif 4217	The symmetric difference contains one of the differences. (Proposed by BJ, 18-Aug-2022.) (Contributed by AV, 19-Aug-2022.)
⊢ (𝐴 ∖ 𝐵) ⊆ (𝐴 △ 𝐵)
Theorem	difsymssdifssd 4218	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 4219	Absorption law for union. (Contributed by NM, 16-Apr-2006.)
⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴
Theorem	inabs 4220	Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
⊢ (𝐴 ∩ (𝐴 ∪ 𝐵)) = 𝐴
Theorem	nssinpss 4221	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 4222	Negation of subclass expressed in terms of proper subclass and union. (Contributed by NM, 15-Sep-2004.)
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ 𝐵 ⊊ (𝐴 ∪ 𝐵))
Theorem	dfss4 4223	Subclass defined in terms of class difference. See comments under dfun2 4224. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴)
Theorem	dfun2 4224	An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 4225 and dfss4 4223 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 4225	An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 4224. Another version is given by dfin4 4232. (Contributed by NM, 10-Jun-2004.)
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵))
Theorem	difin 4226	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 4227	Implication of a class difference with a subclass. (Contributed by AV, 3-Jan-2022.)
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 = (𝑉 ∖ 𝐴)) → 𝐴 = (𝑉 ∖ 𝐵))
Theorem	ssdifsym 4228	Symmetric class differences for subclasses. (Contributed by AV, 3-Jan-2022.)
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 ⊆ 𝑉) → (𝐵 = (𝑉 ∖ 𝐴) ↔ 𝐴 = (𝑉 ∖ 𝐵)))
Theorem	dfss5 4229*	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 4230	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 4231	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 4232	Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.)
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵))
Theorem	invdif 4233	Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
Theorem	indif 4234	Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∖ 𝐵)
Theorem	indif2 4235	Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
Theorem	indif1 4236	Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
Theorem	indifcom 4237	Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = (𝐵 ∩ (𝐴 ∖ 𝐶))
Theorem	indi 4238	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 4239	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 4240	Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶))
Theorem	undir 4241	Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
⊢ ((𝐴 ∩ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∩ (𝐵 ∪ 𝐶))
Theorem	unineq 4242	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 4243	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 4244	Distributive law for class difference. Theorem 39 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∩ (𝐴 ∖ 𝐶))
Theorem	difundir 4245	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
Theorem	difindi 4246	Distributive law for class difference. Theorem 40 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶))
Theorem	difindir 4247	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (𝐵 ∖ 𝐶))
Theorem	indifdi 4248	Distribute intersection over difference. (Contributed by BTernaryTau, 14-Aug-2024.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ (𝐴 ∩ 𝐶))
Theorem	indifdir 4249	Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.) (Revised by BTernaryTau, 14-Aug-2024.)
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶))
Theorem	difdif2 4250	Class difference by a class difference. (Contributed by Thierry Arnoux, 18-Dec-2017.)
⊢ (𝐴 ∖ (𝐵 ∖ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∩ 𝐶))
Theorem	undm 4251	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 4252	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 4253	A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.)
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∖ 𝐶)
Theorem	undif3 4254	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 4255	Represent a class difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = ((𝐶 ∖ 𝐵) ∩ 𝐴))
Theorem	dif32 4256	Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.)
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵)
Theorem	difabs 4257	Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009.)
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)
Theorem	sscon34b 4258	Relative complementation reverses inclusion of subclasses. Relativized version of complss 4105. (Contributed by RP, 3-Jun-2021.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)))
Theorem	rcompleq 4259	Two subclasses are equal if and only if their relative complements are equal. Relativized version of compleq 4106. (Contributed by RP, 10-Jun-2021.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 = 𝐵 ↔ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)))
Theorem	dfsymdif3 4260	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 4261*	Union of two class abstractions. Version of unab 4262 using implicit substitution, which does not require ax-8 2116, ax-10 2147, ax-12 2185. (Contributed by GG, 15-Oct-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    ⇒   ⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑦 ∣ (𝜒 ∨ 𝜃)}
Theorem	unab 4262	Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)}
Theorem	inab 4263	Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∩ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ 𝜓)}
Theorem	difab 4264	Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∖ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ ¬ 𝜓)}
Theorem	abanssl 4265	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 4266	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 4267*	A class abstraction defined by a negation. Version of notab 4268 using implicit substitution, which does not require ax-10 2147, ax-12 2185. (Contributed by GG, 15-Oct-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑦 ∣ 𝜓})
Theorem	notab 4268	A class abstraction defined by a negation. (Contributed by FL, 18-Sep-2010.)
⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑥 ∣ 𝜑})
Theorem	unrab 4269	Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)}
Theorem	inrab 4270	Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	inrab2 4271*	Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑}
Theorem	difrab 4272	Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)}
Theorem	dfrab3 4273*	Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑})
Theorem	dfrab2 4274*	Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.) (Proof shortened by BJ, 22-Apr-2019.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴)
Theorem	rabdif 4275*	Move difference in and out of a restricted class abstraction. (Contributed by Steven Nguyen, 6-Jun-2023.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ 𝐵) = {𝑥 ∈ (𝐴 ∖ 𝐵) ∣ 𝜑}
Theorem	notrab 4276*	Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}
Theorem	dfrab3ss 4277*	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 4278	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 4279	Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Wolf Lammen, 15-May-2025.)
⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑))
Theorem	reuss2 4280*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005.)
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuss 4281*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuun1 4282*	Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.)
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reupick 4283*	Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.)
⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	reupick3 4284*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.)
⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓))
Theorem	reupick2 4285*	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 4286*	Transfer uniqueness of an element to a smaller subclass. (Contributed by AV, 14-Apr-2020.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴 ∧ ∃!𝑥 𝑥 ∈ 𝐵) → ∃!𝑥 𝑥 ∈ 𝐴)
2.1.14  The empty set
Syntax	c0 4287	Extend class notation to include the empty set.
class ∅
Definition	df-nul 4288	Define the empty set. More precisely, we should write "empty class". It will be posited in ax-nul 5253 that an empty set exists. Then, by uniqueness among classes (eq0 4304, as opposed to the weaker uniqueness among sets, nulmo 2714), it will follow that ∅ is indeed a set (0ex 5254). Special case of Exercise 4.10(o) of [Mendelson] p. 231. For a more traditional definition, but requiring a dummy variable, see dfnul2 4290. (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)
Theorem	dfnul4 4289	Alternate definition of the empty class/set. (Contributed by BJ, 30-Nov-2019.) Avoid ax-8 2116, df-clel 2812. (Revised by GG, 3-Sep-2024.) Prove directly from definition to allow shortening dfnul2 4290. (Revised by BJ, 23-Sep-2024.)
⊢ ∅ = {𝑥 ∣ ⊥}
Theorem	dfnul2 4290	Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.) Remove dependency on ax-10 2147, ax-11 2163, and ax-12 2185. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.)
⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
Theorem	dfnul3 4291	Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.) (Proof shortened by BJ, 23-Sep-2024.)
⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴}
Theorem	noel 4292	The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) Remove dependency on ax-10 2147, ax-11 2163, and ax-12 2185. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.)
⊢ ¬ 𝐴 ∈ ∅
Theorem	nel02 4293	The empty set has no elements. (Contributed by Peter Mazsa, 4-Jan-2018.)
⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
Theorem	n0i 4294	If a class has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)
Theorem	ne0i 4295	If a class has elements, then it is nonempty. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)
Theorem	ne0d 4296	Deduction form of ne0i 4295. If a class has elements, then it is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ≠ ∅)
Theorem	n0ii 4297	If a class has elements, then it is not empty. Inference associated with n0i 4294. (Contributed by BJ, 15-Jul-2021.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ ¬ 𝐵 = ∅
Theorem	ne0ii 4298	If a class has elements, then it is nonempty. Inference associated with ne0i 4295. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ 𝐵 ≠ ∅
Theorem	vn0 4299	The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008.) Avoid ax-8 2116, df-clel 2812. (Revised by GG, 6-Sep-2024.)
⊢ V ≠ ∅
Theorem	vn0ALT 4300	Alternate proof of vn0 4299. Shorter, but requiring df-clel 2812, ax-8 2116. (Contributed by NM, 11-Sep-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ V ≠ ∅