P. 49 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4801-4900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	preq12nebg 4801	Equality relationship for two proper unordered pairs. (Contributed by AV, 12-Jun-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
Theorem	prel12g 4802	Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996.) (Revised by AV, 9-Dec-2018.) (Revised by AV, 12-Jun-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))
Theorem	opthprneg 4803	An unordered pair has the ordered pair property (compare opth 5423) under certain conditions. Variant of opthpr 4789 in closed form. (Contributed by AV, 13-Jun-2022.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐷)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	elpreqprlem 4804*	Lemma for elpreqpr 4805. (Contributed by Scott Fenton, 7-Dec-2020.) (Revised by AV, 9-Dec-2020.)
⊢ (𝐵 ∈ 𝑉 → ∃𝑥{𝐵, 𝐶} = {𝐵, 𝑥})
Theorem	elpreqpr 4805*	Equality and membership rule for pairs. (Contributed by Scott Fenton, 7-Dec-2020.)
⊢ (𝐴 ∈ {𝐵, 𝐶} → ∃𝑥{𝐵, 𝐶} = {𝐴, 𝑥})
Theorem	elpreqprb 4806*	A set is an element of an unordered pair iff there is another (maybe the same) set which is an element of the unordered pair. (Proposed by BJ, 8-Dec-2020.) (Contributed by AV, 9-Dec-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ ∃𝑥{𝐵, 𝐶} = {𝐴, 𝑥}))
Theorem	elpr2elpr 4807*	For an element 𝐴 of an unordered pair which is a subset of a given set 𝑉, there is another (maybe the same) element 𝑏 of the given set 𝑉 being an element of the unordered pair. (Contributed by AV, 5-Dec-2020.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ {𝑋, 𝑌}) → ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝐴, 𝑏})
Theorem	dfopif 4808	Rewrite df-op 4569 using if. When both arguments are sets, it reduces to the standard Kuratowski definition; otherwise, it is defined to be the empty set. Avoid directly depending on this detail so that theorems will not depend on the Kuratowski construction. (Contributed by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.)
⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
Theorem	dfopg 4809	Value of the ordered pair when the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
Theorem	dfop 4810	Value of an ordered pair when the arguments are sets, with the conclusion corresponding to Kuratowski's original definition. (Contributed by NM, 25-Jun-1998.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}}
Theorem	opeq1 4811	Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Theorem	opeq2 4812	Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Theorem	opeq12 4813	Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
Theorem	opeq1i 4814	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩
Theorem	opeq2i 4815	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩
Theorem	opeq12i 4816	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩
Theorem	opeq1d 4817	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Theorem	opeq2d 4818	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Theorem	opeq12d 4819	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
Theorem	oteq1 4820	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶, 𝐷⟩ = ⟨𝐵, 𝐶, 𝐷⟩)
Theorem	oteq2 4821	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴, 𝐷⟩ = ⟨𝐶, 𝐵, 𝐷⟩)
Theorem	oteq3 4822	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)
Theorem	oteq1d 4823	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐶, 𝐷⟩ = ⟨𝐵, 𝐶, 𝐷⟩)
Theorem	oteq2d 4824	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐴, 𝐷⟩ = ⟨𝐶, 𝐵, 𝐷⟩)
Theorem	oteq3d 4825	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)
Theorem	oteq123d 4826	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐶, 𝐸⟩ = ⟨𝐵, 𝐷, 𝐹⟩)
Theorem	nfop 4827	Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩
Theorem	nfopd 4828	Deduction version of bound-variable hypothesis builder nfop 4827. This shows how the deduction version of a not-free theorem such as nfop 4827 can be created from the corresponding not-free inference theorem. (Contributed by NM, 4-Feb-2008.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥⟨𝐴, 𝐵⟩)
Theorem	csbopg 4829	Distribution of class substitution over ordered pairs. (Contributed by Drahflow, 25-Sep-2015.) (Revised by Mario Carneiro, 29-Oct-2015.) (Revised by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⟨𝐶, 𝐷⟩ = ⟨⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷⟩)
Theorem	opidg 4830	The ordered pair ⟨𝐴, 𝐴⟩ in Kuratowski's representation. Closed form of opid 4831. (Contributed by Peter Mazsa, 22-Jul-2019.) (Avoid depending on this detail.)
⊢ (𝐴 ∈ 𝑉 → ⟨𝐴, 𝐴⟩ = {{𝐴}})
Theorem	opid 4831	The ordered pair ⟨𝐴, 𝐴⟩ in Kuratowski's representation. Inference form of opidg 4830. (Contributed by FL, 28-Dec-2011.) (Proof shortened by AV, 16-Feb-2022.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ⟨𝐴, 𝐴⟩ = {{𝐴}}
Theorem	ralunsn 4832*	Restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)))
Theorem	2ralunsn 4833*	Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})∀𝑦 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) ∧ (∀𝑦 ∈ 𝐴 𝜒 ∧ 𝜃))))
Theorem	opprc 4834	Expansion of an ordered pair when either member is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐴, 𝐵⟩ = ∅)
Theorem	opprc1 4835	Expansion of an ordered pair when the first member is a proper class. See also opprc 4834. (Contributed by NM, 10-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (¬ 𝐴 ∈ V → ⟨𝐴, 𝐵⟩ = ∅)
Theorem	opprc2 4836	Expansion of an ordered pair when the second member is a proper class. See also opprc 4834. (Contributed by NM, 15-Nov-1994.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (¬ 𝐵 ∈ V → ⟨𝐴, 𝐵⟩ = ∅)
Theorem	oprcl 4837	If an ordered pair has an element, then its arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐶 ∈ ⟨𝐴, 𝐵⟩ → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	pwsn 4838	The power set of a singleton. (Contributed by NM, 5-Jun-2006.)
⊢ 𝒫 {𝐴} = {∅, {𝐴}}
Theorem	pwpr 4839	The power set of an unordered pair. (Contributed by NM, 1-May-2009.)
⊢ 𝒫 {𝐴, 𝐵} = ({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}})
Theorem	pwtp 4840	The power set of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ 𝒫 {𝐴, 𝐵, 𝐶} = (({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) ∪ ({{𝐶}, {𝐴, 𝐶}} ∪ {{𝐵, 𝐶}, {𝐴, 𝐵, 𝐶}}))
Theorem	pwpwpw0 4841	Compute the power set of the power set of the power set of the empty set. (See also pw0 4750 and pwpw0 4751.) (Contributed by NM, 2-May-2009.)
⊢ 𝒫 {∅, {∅}} = ({∅, {∅}} ∪ {{{∅}}, {∅, {∅}}})
Theorem	pwv 4842	The power class of the universe is the universe. Exercise 4.12(d) of [Mendelson] p. 235. The collection of all classes is of course larger than V, which is the collection of all sets. But 𝒫 V, being a class, cannot contain proper classes, so 𝒫 V is actually no larger than V. This fact is exploited in ncanth 7318. (Contributed by NM, 14-Sep-2003.)
⊢ 𝒫 V = V
Theorem	prproe 4843*	For an element of a proper unordered pair of elements of a class 𝑉, there is another (different) element of the class 𝑉 which is an element of the proper pair. (Contributed by AV, 18-Dec-2021.)
⊢ ((𝐶 ∈ {𝐴, 𝐵} ∧ 𝐴 ≠ 𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ∃𝑣 ∈ (𝑉 ∖ {𝐶})𝑣 ∈ {𝐴, 𝐵})
Theorem	3elpr2eq 4844	If there are three elements in a proper unordered pair, and two of them are different from the third one, the two must be equal. (Contributed by AV, 19-Dec-2021.)
⊢ (((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) ∧ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋)) → 𝑌 = 𝑍)
2.1.19  The union of a class
Syntax	cuni 4845	Extend class notation to include the union of a class. Read: "union (of) 𝐴".
class ∪ 𝐴
Definition	df-uni 4846*	Define the union of a class i.e. the collection of all members of the members of the class. Definition 5.5 of [TakeutiZaring] p. 16. For example, ∪ {{1, 3}, {1, 8}} = {1, 3, 8} (ex-uni 30521). This is similar to the union of two classes df-un 3895. (Contributed by NM, 23-Aug-1993.)
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)}
Theorem	dfuni2 4847*	Alternate definition of class union. (Contributed by NM, 28-Jun-1998.)
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
Theorem	eluni 4848*	Membership in class union. (Contributed by NM, 22-May-1994.)
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
Theorem	eluni2 4849*	Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)
Theorem	elunii 4850	Membership in class union. (Contributed by NM, 24-Mar-1995.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)
Theorem	nfunid 4851	Deduction version of nfuni 4852. (Contributed by NM, 18-Feb-2013.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴)
Theorem	nfuni 4852	Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥∪ 𝐴
Theorem	uniss 4853	Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
Theorem	unissi 4854	Subclass relationship for subclass union. Inference form of uniss 4853. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ∪ 𝐴 ⊆ ∪ 𝐵
Theorem	unissd 4855	Subclass relationship for subclass union. Deduction form of uniss 4853. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵)
Theorem	unieq 4856	Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by BJ, 13-Apr-2024.)
⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
Theorem	unieqi 4857	Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∪ 𝐴 = ∪ 𝐵
Theorem	unieqd 4858	Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)
Theorem	eluniab 4859*	Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑))
Theorem	elunirab 4860*	Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006.)
⊢ (𝐴 ∈ ∪ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝜑))
Theorem	uniprg 4861	The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 25-Aug-2006.) Avoid using unipr 4862 to prove it from uniprg 4861. (Revised by BJ, 1-Sep-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
Theorem	unipr 4862	The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 23-Aug-1993.) (Proof shortened by BJ, 1-Sep-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
Theorem	unisng 4863	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.)
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)
Theorem	unisn 4864	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∪ {𝐴} = 𝐴
Theorem	unisnv 4865	A set equals the union of its singleton (setvar case). (Contributed by NM, 30-Aug-1993.)
⊢ ∪ {𝑥} = 𝑥
Theorem	unisn3 4866*	Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.)
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 = 𝐴} = 𝐴)
Theorem	dfnfc2 4867*	An alternative statement of the effective freeness of a class 𝐴, when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.) (Proof shortened by JJ, 26-Jul-2021.)
⊢ (∀𝑥 𝐴 ∈ 𝑉 → (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴))
Theorem	uniun 4868	The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.)
⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵)
Theorem	uniin 4869	The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235. See uniinqs 8741 for a condition where equality holds. (Contributed by NM, 4-Dec-2003.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ ∪ (𝐴 ∩ 𝐵) ⊆ (∪ 𝐴 ∩ ∪ 𝐵)
Theorem	ssuni 4870	Subclass relationship for class union. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 26-Jul-2021.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ⊆ ∪ 𝐶)
Theorem	uni0b 4871	The union of a set is empty iff the set is included in the singleton of the empty set. (Contributed by NM, 12-Sep-2004.)
⊢ (∪ 𝐴 = ∅ ↔ 𝐴 ⊆ {∅})
Theorem	uni0c 4872*	The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006.)
⊢ (∪ 𝐴 = ∅ ↔ ∀𝑥 ∈ 𝐴 𝑥 = ∅)
Theorem	uni0 4873	The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Contributed by NM, 16-Sep-1993.) Remove use of ax-nul 5235. (Revised by Eric Schmidt, 4-Apr-2007.) Avoid ax-11 2168. (Revised by TM, 1-Feb-2026.)
⊢ ∪ ∅ = ∅
Theorem	uni0OLD 4874	Obsolete version of uni0 4873 as of 1-Feb-2026. (Contributed by NM, 16-Sep-1993.) Remove use of ax-nul 5235. (Revised by Eric Schmidt, 4-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∪ ∅ = ∅
Theorem	csbuni 4875	Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 22-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌∪ 𝐵 = ∪ ⦋𝐴 / 𝑥⦌𝐵
Theorem	elssuni 4876	An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Jun-1994.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝐵)
Theorem	unissel 4877	Condition turning a subclass relationship for union into an equality. (Contributed by NM, 18-Jul-2006.)
⊢ ((∪ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐴) → ∪ 𝐴 = 𝐵)
Theorem	unissb 4878*	Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.) Avoid ax-11 2168. (Revised by BTernaryTau, 28-Dec-2024.)
⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
Theorem	uniss2 4879*	A subclass condition on the members of two classes that implies a subclass relation on their unions. Proposition 8.6 of [TakeutiZaring] p. 59. See iunss2 4986 for a generalization to indexed unions. (Contributed by NM, 22-Mar-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∪ 𝐴 ⊆ ∪ 𝐵)
Theorem	unidif 4880*	If the difference 𝐴 ∖ 𝐵 contains the largest members of 𝐴, then the union of the difference is the union of 𝐴. (Contributed by NM, 22-Mar-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐴 ∖ 𝐵)𝑥 ⊆ 𝑦 → ∪ (𝐴 ∖ 𝐵) = ∪ 𝐴)
Theorem	ssunieq 4881*	Relationship implying union. (Contributed by NM, 10-Nov-1999.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝑥 ⊆ 𝐴) → 𝐴 = ∪ 𝐵)
Theorem	unimax 4882*	Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002.)
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} = 𝐴)
Theorem	pwuni 4883	A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.)
⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
2.1.20  The intersection of a class
Syntax	cint 4884	Extend class notation to include the intersection of a class. Read: "intersection (of) 𝐴".
class ∩ 𝐴
Definition	df-int 4885*	Define the intersection of a class. Definition 7.35 of [TakeutiZaring] p. 44. For example, ∩ {{1, 3}, {1, 8}} = {1}. Compare this with the intersection of two classes, df-in 3897. (Contributed by NM, 18-Aug-1993.)
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)}
Theorem	dfint2 4886*	Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998.)
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
Theorem	inteq 4887	Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)
Theorem	inteqi 4888	Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∩ 𝐴 = ∩ 𝐵
Theorem	inteqd 4889	Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)
Theorem	elint 4890*	Membership in class intersection. (Contributed by NM, 21-May-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥))
Theorem	elint2 4891*	Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)
Theorem	elintg 4892*	Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.) (Proof shortened by JJ, 26-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥))
Theorem	elinti 4893	Membership in class intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝐴 ∈ ∩ 𝐵 → (𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶))
Theorem	nfint 4894	Bound-variable hypothesis builder for intersection. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥∩ 𝐴
Theorem	elintabg 4895*	Two ways of saying a set is an element of the intersection of a class. (Contributed by NM, 30-Aug-1993.) Put in closed form. (Revised by RP, 13-Aug-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))
Theorem	elintab 4896*	Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))
Theorem	elintrab 4897*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥))
Theorem	elintrabg 4898*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Feb-2007.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥)))
Theorem	int0 4899	The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44. (Contributed by NM, 18-Aug-1993.) (Proof shortened by JJ, 26-Jul-2021.)
⊢ ∩ ∅ = V
Theorem	intss1 4900	An element of a class includes the intersection of the class. Exercise 4 of [TakeutiZaring] p. 44 (with correction), generalized to classes. (Contributed by NM, 18-Nov-1995.)
⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)