P. 50 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4901-5000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfint2 4901*	Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998.)
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
Theorem	inteq 4902	Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)
Theorem	inteqi 4903	Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∩ 𝐴 = ∩ 𝐵
Theorem	inteqd 4904	Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)
Theorem	elint 4905*	Membership in class intersection. (Contributed by NM, 21-May-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥))
Theorem	elint2 4906*	Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)
Theorem	elintg 4907*	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 4908	Membership in class intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝐴 ∈ ∩ 𝐵 → (𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶))
Theorem	nfint 4909	Bound-variable hypothesis builder for intersection. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥∩ 𝐴
Theorem	elintabg 4910*	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 4911*	Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))
Theorem	elintabOLD 4912*	Obsolete version of elintab 4911 as of 17-Jan-2025. (Contributed by NM, 30-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))
Theorem	elintrab 4913*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥))
Theorem	elintrabg 4914*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Feb-2007.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥)))
Theorem	int0 4915	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 4916	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.)
⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)
Theorem	ssint 4917*	Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥)
Theorem	ssintab 4918*	Subclass of the intersection of a class abstraction. (Contributed by NM, 31-Jul-2006.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝐴 ⊆ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ⊆ 𝑥))
Theorem	ssintub 4919*	Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}
Theorem	ssmin 4920*	Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006.)
⊢ 𝐴 ⊆ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)}
Theorem	intmin 4921*	Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} = 𝐴)
Theorem	intss 4922	Intersection of subclasses. (Contributed by NM, 14-Oct-1999.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴)
Theorem	intssuni 4923	The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006.)
⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)
Theorem	ssintrab 4924*	Subclass of the intersection of a restricted class abstraction. (Contributed by NM, 30-Jan-2015.)
⊢ (𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ⊆ 𝑥))
Theorem	unissint 4925	If the union of a class is included in its intersection, the class is either the empty set or a singleton (uniintsn 4938). (Contributed by NM, 30-Oct-2010.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∪ 𝐴 ⊆ ∩ 𝐴 ↔ (𝐴 = ∅ ∨ ∪ 𝐴 = ∩ 𝐴))
Theorem	intssuni2 4926	Subclass relationship for intersection and union. (Contributed by NM, 29-Jul-2006.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ⊆ ∪ 𝐵)
Theorem	intminss 4927*	Under subset ordering, the intersection of a restricted class abstraction is less than or equal to any of its members. (Contributed by NM, 7-Sep-2013.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ⊆ 𝐴)
Theorem	intmin2 4928*	Any set is the smallest of all sets that include it. (Contributed by NM, 20-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ 𝐴 ⊆ 𝑥} = 𝐴
Theorem	intmin3 4929*	Under subset ordering, the intersection of a class abstraction is less than or equal to any of its members. (Contributed by NM, 3-Jul-2005.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∩ {𝑥 ∣ 𝜑} ⊆ 𝐴)
Theorem	intmin4 4930*	Elimination of a conjunct in a class intersection. (Contributed by NM, 31-Jul-2006.)
⊢ (𝐴 ⊆ ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} = ∩ {𝑥 ∣ 𝜑})
Theorem	intab 4931*	The intersection of a special case of a class abstraction. 𝑦 may be free in 𝜑 and 𝐴, which can be thought of a 𝜑(𝑦) and 𝐴(𝑦). Typically, abrexex2 7911 or abexssex 7912 can be used to satisfy the second hypothesis. (Contributed by NM, 28-Jul-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
⊢ 𝐴 ∈ V    &   ⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}
Theorem	int0el 4932	The intersection of a class containing the empty set is empty. (Contributed by NM, 24-Apr-2004.)
⊢ (∅ ∈ 𝐴 → ∩ 𝐴 = ∅)
Theorem	intun 4933	The class intersection of the union of two classes. Theorem 78 of [Suppes] p. 42. (Contributed by NM, 22-Sep-2002.)
⊢ ∩ (𝐴 ∪ 𝐵) = (∩ 𝐴 ∩ ∩ 𝐵)
Theorem	intprg 4934	The intersection of a pair is the intersection of its members. Closed form of intpr 4935. Theorem 71 of [Suppes] p. 42. (Contributed by FL, 27-Apr-2008.) (Proof shortened by BJ, 1-Sep-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
Theorem	intpr 4935	The intersection of a pair is the intersection of its members. Theorem 71 of [Suppes] p. 42. (Contributed by NM, 14-Oct-1999.) Prove from intprg 4934. (Revised by BJ, 1-Sep-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵)
Theorem	intsng 4936	Intersection of a singleton. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴)
Theorem	intsn 4937	The intersection of a singleton is its member. Theorem 70 of [Suppes] p. 41. (Contributed by NM, 29-Sep-2002.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝐴} = 𝐴
Theorem	uniintsn 4938*	Two ways to express "𝐴 is a singleton". See also en1 8956, en1b 8957, card1 9883, and eusn 4684. (Contributed by NM, 2-Aug-2010.)
⊢ (∪ 𝐴 = ∩ 𝐴 ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	uniintab 4939	The union and the intersection of a class abstraction are equal exactly when there is a unique satisfying value of 𝜑(𝑥). (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (∃!𝑥𝜑 ↔ ∪ {𝑥 ∣ 𝜑} = ∩ {𝑥 ∣ 𝜑})
Theorem	intunsn 4940	Theorem joining a singleton to an intersection. (Contributed by NM, 29-Sep-2002.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ (𝐴 ∪ {𝐵}) = (∩ 𝐴 ∩ 𝐵)
Theorem	rint0 4941	Relative intersection of an empty set. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩ 𝑋) = 𝐴)
Theorem	elrint 4942*	Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦))
Theorem	elrint2 4943*	Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 ∈ 𝐴 → (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦))
2.1.21  Indexed union and intersection
Syntax	ciun 4944	Extend class notation to include indexed union. Note: Historically (prior to 21-Oct-2005), set.mm used the notation ∪ 𝑥 ∈ 𝐴𝐵, with the same union symbol as cuni 4861. While that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses a distinguished symbol ∪ instead of ∪ and does allow LALR parsing. Thanks to Peter Backes for suggesting this change.
class ∪ 𝑥 ∈ 𝐴 𝐵
Syntax	ciin 4945	Extend class notation to include indexed intersection. Note: Historically (prior to 21-Oct-2005), set.mm used the notation ∩ 𝑥 ∈ 𝐴𝐵, with the same intersection symbol as cint 4899. Although that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses a distinguished symbol ∩ instead of ∩ and does allow LALR parsing. Thanks to Peter Backes for suggesting this change.
class ∩ 𝑥 ∈ 𝐴 𝐵
Definition	df-iun 4946*	Define indexed union. Definition indexed union in [Stoll] p. 45. In most applications, 𝐴 is independent of 𝑥 (although this is not required by the definition), and 𝐵 depends on 𝑥 i.e. can be read informally as 𝐵(𝑥). We call 𝑥 the index, 𝐴 the index set, and 𝐵 the indexed set. In most books, 𝑥 ∈ 𝐴 is written as a subscript or underneath a union symbol ∪. We use a special union symbol ∪ to make it easier to distinguish from plain class union. In many theorems, you will see that 𝑥 and 𝐴 are in the same distinct variable group (meaning 𝐴 cannot depend on 𝑥) and that 𝐵 and 𝑥 do not share a distinct variable group (meaning that can be thought of as 𝐵(𝑥) i.e. can be substituted with a class expression containing 𝑥). An alternate definition tying indexed union to ordinary union is dfiun2 4985. Theorem uniiun 5010 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7187 and funiunfv 7188 are useful when 𝐵 is a function. (Contributed by NM, 27-Jun-1998.)
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
Definition	df-iin 4947*	Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4946. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4986. Theorem intiin 5011 provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998.)
⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
Theorem	eliun 4948*	Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)
Theorem	eliin 4949*	Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
Theorem	eliuni 4950*	Membership in an indexed union, one way. (Contributed by JJ, 27-Jul-2021.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ 𝐶) → 𝐸 ∈ ∪ 𝑥 ∈ 𝐷 𝐵)
Theorem	eliund 4951*	Membership in indexed union. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	iuncom 4952*	Commutation of indexed unions. (Contributed by NM, 18-Dec-2008.)
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = ∪ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶
Theorem	iuncom4 4953	Commutation of union with indexed union. (Contributed by Mario Carneiro, 18-Jan-2014.)
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 = ∪ ∪ 𝑥 ∈ 𝐴 𝐵
Theorem	iunconst 4954*	Indexed union of a constant class, i.e. where 𝐵 does not depend on 𝑥. (Contributed by NM, 5-Sep-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ≠ ∅ → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐵)
Theorem	iinconst 4955*	Indexed intersection of a constant class, i.e. where 𝐵 does not depend on 𝑥. (Contributed by Mario Carneiro, 6-Feb-2015.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 = 𝐵)
Theorem	iuneqconst 4956*	Indexed union of identical classes. (Contributed by AV, 5-Mar-2024.)
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶)
Theorem	iuniin 4957*	Law combining indexed union with indexed intersection. Eq. 14 in [KuratowskiMostowski] p. 109. This theorem also appears as the last example at http://en.wikipedia.org/wiki/Union%5F%28set%5Ftheory%29. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ∪ 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ⊆ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶
Theorem	iinssiun 4958*	An indexed intersection is a subset of the corresponding indexed union. (Contributed by Thierry Arnoux, 31-Dec-2021.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iunss1 4959*	Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	iinss1 4960*	Subclass theorem for indexed intersection. (Contributed by NM, 24-Jan-2012.)
⊢ (𝐴 ⊆ 𝐵 → ∩ 𝑥 ∈ 𝐵 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq1 4961*	Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.)
⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	iineq1 4962*	Equality theorem for indexed intersection. (Contributed by NM, 27-Jun-1998.)
⊢ (𝐴 = 𝐵 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶)
Theorem	ss2iun 4963	Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq2 4964	Equality theorem for indexed union. (Contributed by NM, 22-Oct-2003.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iineq2 4965	Equality theorem for indexed intersection. (Contributed by NM, 22-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq2i 4966	Equality inference for indexed union. (Contributed by NM, 22-Oct-2003.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶
Theorem	iineq2i 4967	Equality inference for indexed intersection. (Contributed by NM, 22-Oct-2003.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶
Theorem	iineq2d 4968	Equality deduction for indexed intersection. (Contributed by NM, 7-Dec-2011.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq2dv 4969*	Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iineq2dv 4970*	Equality deduction for indexed intersection. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq12df 4971	Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 31-Dec-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iuneq1d 4972*	Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	iuneq12dOLD 4973*	Obsolete version of iuneq12d 4974 as of 1-Sep-2025. (Contributed by Drahflow, 22-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iuneq12d 4974*	Equality deduction for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.) Remove DV conditions (Revised by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iuneq2d 4975*	Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	nfiun 4976*	Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2370. See nfiung 4978 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiin 4977*	Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2370. See nfiing 4979 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiung 4978	Bound-variable hypothesis builder for indexed union. Usage of this theorem is discouraged because it depends on ax-13 2370. See nfiun 4976 for a version with more disjoint variable conditions, but not requiring ax-13 2370. (Contributed by Mario Carneiro, 25-Jan-2014.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiing 4979	Bound-variable hypothesis builder for indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 2370. See nfiin 4977 for a version with more disjoint variable conditions, but not requiring ax-13 2370. (Contributed by Mario Carneiro, 25-Jan-2014.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiu1 4980	Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2158, ax-12 2178. (Revised by SN, 14-May-2025.)
⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiu1OLD 4981	Obsolete version of nfiu1 4980 as of 14-May-2025. (Contributed by NM, 12-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
Theorem	nfii1 4982	Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.)
⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵
Theorem	dfiun2g 4983*	Alternate definition of indexed union when 𝐵 is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by Rohan Ridenour, 11-Aug-2023.) Avoid ax-10 2142, ax-12 2178. (Revised by SN, 11-Dec-2024.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
Theorem	dfiin2g 4984*	Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Jeff Hankins, 27-Aug-2009.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
Theorem	dfiun2 4985*	Alternate definition of indexed union when 𝐵 is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 27-Jun-1998.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
Theorem	dfiin2 4986*	Alternate definition of indexed intersection when 𝐵 is a set. Definition 15(b) of [Suppes] p. 44. (Contributed by NM, 28-Jun-1998.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
Theorem	dfiunv2 4987*	Define double indexed union. (Contributed by FL, 6-Nov-2013.)
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 ∈ 𝐶}
Theorem	cbviun 4988*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.) Add disjoint variable condition to avoid ax-13 2370. See cbviung 4990 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviin 4989*	Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.) Add disjoint variable condition to avoid ax-13 2370. See cbviing 4991 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviung 4990*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. Usage of this theorem is discouraged because it depends on ax-13 2370. See cbviun 4988 for a version with more disjoint variable conditions, but not requiring ax-13 2370. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviing 4991*	Change bound variables in an indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 2370. See cbviin 4989 for a version with more disjoint variable conditions, but not requiring ax-13 2370. (Contributed by Jeff Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviunv 4992*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 15-Sep-2003.) Add disjoint variable condition to avoid ax-13 2370. See cbviunvg 4994 for a less restrictive version requiring more axioms. (Revised by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviinv 4993*	Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) Add disjoint variable condition to avoid ax-13 2370. See cbviinvg 4995 for a less restrictive version requiring more axioms. (Revised by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviunvg 4994*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. Usage of this theorem is discouraged because it depends on ax-13 2370. Usage of the weaker cbviunv 4992 is preferred. (Contributed by NM, 15-Sep-2003.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviinvg 4995*	Change bound variables in an indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 2370. Usage of the weaker cbviinv 4993 is preferred. (Contributed by Jeff Hankins, 26-Aug-2009.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶
Theorem	iunssf 4996	Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	iunss 4997*	Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	ssiun 4998*	Subset implication for an indexed union. (Contributed by NM, 3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∃𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ssiun2 4999	Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ssiun2s 5000*	Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.)
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)