P. 326 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32501-32600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elabreximd 32501*	Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝐴 = 𝐵 → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐶 𝑦 = 𝐵}) → 𝜒)
Theorem	elabreximdv 32502*	Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ (𝐴 = 𝐵 → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐶 𝑦 = 𝐵}) → 𝜒)
Theorem	abrexss 32503*	A necessary condition for an image set to be a subset. (Contributed by Thierry Arnoux, 6-Feb-2017.)
⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐶)
21.3.3.3  Set relations and operations - misc additions
Theorem	nelun 32504	Negated membership for a union. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ (𝐴 = (𝐵 ∪ 𝐶) → (¬ 𝑋 ∈ 𝐴 ↔ (¬ 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝐶)))
Theorem	snsssng 32505	If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.) (Revised by Thierry Arnoux, 11-Apr-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ {𝐴} ⊆ {𝐵}) → 𝐴 = 𝐵)
Theorem	n0nsnel 32506*	If a class with one element is not a singleton, there is at least another element in this class. (Contributed by AV, 6-Mar-2025.) (Revised by Thierry Arnoux, 28-May-2025.)
⊢ ((𝐶 ∈ 𝐵 ∧ 𝐵 ≠ {𝐴}) → ∃𝑥 ∈ 𝐵 𝑥 ≠ 𝐴)
Theorem	inin 32507	Intersection with an intersection. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ (𝐴 ∩ (𝐴 ∩ 𝐵)) = (𝐴 ∩ 𝐵)
Theorem	difininv 32508	Condition for the intersections of two sets with a given set to be equal. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ ((((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ∧ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅) → (𝐴 ∩ 𝐵) = (𝐶 ∩ 𝐵))
Theorem	difeq 32509	Rewriting an equation with class difference, without using quantifiers. (Contributed by Thierry Arnoux, 24-Sep-2017.)
⊢ ((𝐴 ∖ 𝐵) = 𝐶 ↔ ((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)))
Theorem	eqdif 32510	If both set differences of two sets are empty, those sets are equal. (Contributed by Thierry Arnoux, 16-Nov-2023.)
⊢ (((𝐴 ∖ 𝐵) = ∅ ∧ (𝐵 ∖ 𝐴) = ∅) → 𝐴 = 𝐵)
Theorem	indifbi 32511	Two ways to express equality relative to a class 𝐴. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ ((𝐴 ∩ 𝐵) = (𝐴 ∩ 𝐶) ↔ (𝐴 ∖ 𝐵) = (𝐴 ∖ 𝐶))
Theorem	diffib 32512	Case where diffi 9094 is a biconditional. (Contributed by Thierry Arnoux, 27-Jun-2024.)
⊢ (𝐵 ∈ Fin → (𝐴 ∈ Fin ↔ (𝐴 ∖ 𝐵) ∈ Fin))
Theorem	difxp1ss 32513	Difference law for Cartesian products. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ ((𝐴 ∖ 𝐶) × 𝐵) ⊆ (𝐴 × 𝐵)
Theorem	difxp2ss 32514	Difference law for Cartesian products. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ (𝐴 × (𝐵 ∖ 𝐶)) ⊆ (𝐴 × 𝐵)
Theorem	indifundif 32515	A remarkable equation with sets. (Contributed by Thierry Arnoux, 18-May-2020.)
⊢ (((𝐴 ∩ 𝐵) ∖ 𝐶) ∪ (𝐴 ∖ 𝐵)) = (𝐴 ∖ (𝐵 ∩ 𝐶))
Theorem	elpwincl1 32516	Closure of intersection with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ 𝒫 𝐶)
Theorem	elpwdifcl 32517	Closure of class difference with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ 𝒫 𝐶)
Theorem	elpwiuncl 32518*	Closure of indexed union with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 27-May-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝒫 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝒫 𝐶)
21.3.3.4  Unordered pairs
Theorem	elpreq 32519	Equality wihin a pair. (Contributed by Thierry Arnoux, 23-Aug-2017.)
⊢ (𝜑 → 𝑋 ∈ {𝐴, 𝐵})    &   ⊢ (𝜑 → 𝑌 ∈ {𝐴, 𝐵})    &   ⊢ (𝜑 → (𝑋 = 𝐴 ↔ 𝑌 = 𝐴))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	prssad 32520	If a pair is a subset of a class, the first element of the pair is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	prssbd 32521	If a pair is a subset of a class, the second element of the pair is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝐶)
Theorem	nelpr 32522	A set 𝐴 not in a pair is neither element of the pair. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶)))
Theorem	inpr0 32523	Rewrite an empty intersection with a pair. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ ((𝐴 ∩ {𝐵, 𝐶}) = ∅ ↔ (¬ 𝐵 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴))
Theorem	neldifpr1 32524	The first element of a pair is not an element of a difference with this pair. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ ¬ 𝐴 ∈ (𝐶 ∖ {𝐴, 𝐵})
Theorem	neldifpr2 32525	The second element of a pair is not an element of a difference with this pair. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ ¬ 𝐵 ∈ (𝐶 ∖ {𝐴, 𝐵})
Theorem	unidifsnel 32526	The other element of a pair is an element of the pair. (Contributed by Thierry Arnoux, 26-Aug-2017.)
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {𝑋}) ∈ 𝑃)
Theorem	unidifsnne 32527	The other element of a pair is not the known element. (Contributed by Thierry Arnoux, 26-Aug-2017.)
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {𝑋}) ≠ 𝑋)
21.3.3.5  Unordered triples
Theorem	tpssg 32528	An unordered triple of elements of a class is a subset of the class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ↔ {𝐴, 𝐵, 𝐶} ⊆ 𝐷))
Theorem	tpssd 32529	Deduction version of tpssi : An unordered triple of elements of a class is a subset of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)
Theorem	tpssad 32530	If an ordered triple is a subset of a class, the first element of the triple is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐷)
Theorem	tpssbd 32531	If an ordered triple is a subset of a class, the second element of the triple is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝐷)
Theorem	tpsscd 32532	If an ordered triple is a subset of a class, the third element of the triple is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
21.3.3.6  Conditional operator - misc additions
Theorem	ifeqeqx 32533*	An equality theorem tailored for ballotlemsf1o 34538. (Contributed by Thierry Arnoux, 14-Apr-2017.)
⊢ (𝑥 = 𝑋 → 𝐴 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝑎)    &   ⊢ (𝑥 = 𝑋 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑌 → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → 𝑎 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    ⇒   ⊢ ((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵))
Theorem	elimifd 32534	Elimination of a conditional operator contained in a wff 𝜒. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → (if(𝜓, 𝐴, 𝐵) = 𝐴 → (𝜒 ↔ 𝜃)))    &   ⊢ (𝜑 → (if(𝜓, 𝐴, 𝐵) = 𝐵 → (𝜒 ↔ 𝜏)))    ⇒   ⊢ (𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜃) ∨ (¬ 𝜓 ∧ 𝜏))))
Theorem	elim2if 32535	Elimination of two conditional operators contained in a wff 𝜒. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐴 → (𝜒 ↔ 𝜃))    &   ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐵 → (𝜒 ↔ 𝜏))    &   ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐶 → (𝜒 ↔ 𝜂))    ⇒   ⊢ (𝜒 ↔ ((𝜑 ∧ 𝜃) ∨ (¬ 𝜑 ∧ ((𝜓 ∧ 𝜏) ∨ (¬ 𝜓 ∧ 𝜂)))))
Theorem	elim2ifim 32536	Elimination of two conditional operators for an implication. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐴 → (𝜒 ↔ 𝜃))    &   ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐵 → (𝜒 ↔ 𝜏))    &   ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐶 → (𝜒 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜏)    &   ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜂)    ⇒   ⊢ 𝜒
Theorem	ifeq3da 32537	Given an expression 𝐶 containing if(𝜓, 𝐸, 𝐹), substitute (hypotheses .1 and .2) and evaluate (hypotheses .3 and .4) it for both cases at the same time. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ (if(𝜓, 𝐸, 𝐹) = 𝐸 → 𝐶 = 𝐺)    &   ⊢ (if(𝜓, 𝐸, 𝐹) = 𝐹 → 𝐶 = 𝐻)    &   ⊢ (𝜑 → 𝐺 = 𝐴)    &   ⊢ (𝜑 → 𝐻 = 𝐵)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)
Theorem	ifnetrue 32538	Deduce truth from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴) → 𝜑)
Theorem	ifnefals 32539	Deduce falsehood from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵) → ¬ 𝜑)
Theorem	ifnebib 32540	The converse of ifbi 4499 holds if the two values are not equal. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ (𝐴 ≠ 𝐵 → (if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵) ↔ (𝜑 ↔ 𝜓)))
21.3.3.7  Set union
Theorem	uniinn0 32541*	Sufficient and necessary condition for a union to intersect with a given set. (Contributed by Thierry Arnoux, 27-Jan-2020.)
⊢ ((∪ 𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐵) ≠ ∅)
Theorem	uniin1 32542*	Union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝑥 ∩ 𝐵) = (∪ 𝐴 ∩ 𝐵)
Theorem	uniin2 32543*	Union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ ∪ 𝑥 ∈ 𝐵 (𝐴 ∩ 𝑥) = (𝐴 ∩ ∪ 𝐵)
Theorem	difuncomp 32544	Express a class difference using unions and class complements. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = (𝐶 ∖ ((𝐶 ∖ 𝐴) ∪ 𝐵)))
Theorem	elpwunicl 32545	Closure of a set union with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 21-Jun-2020.) (Proof shortened by BJ, 6-Apr-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝒫 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝒫 𝐵)
21.3.3.8  Indexed union - misc additions
Theorem	cbviunf 32546*	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.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶
Theorem	iuneq12daf 32547	Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 13-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iunin1f 32548	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5011 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.) (Revised by Thierry Arnoux, 2-May-2020.)
⊢ Ⅎ𝑥𝐶    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶)
Theorem	ssiun3 32549*	Subset equivalence for an indexed union. (Contributed by Thierry Arnoux, 17-Oct-2016.)
⊢ (∀𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ssiun2sf 32550	Subset relationship for an indexed union. (Contributed by Thierry Arnoux, 31-Dec-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iuninc 32551*	The union of an increasing collection of sets is its last element. (Contributed by Thierry Arnoux, 22-Jan-2017.)
⊢ (𝜑 → 𝐹 Fn ℕ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖))
Theorem	iundifdifd 32552*	The intersection of a set is the complement of the union of the complements. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ (𝐴 ⊆ 𝒫 𝑂 → (𝐴 ≠ ∅ → ∩ 𝐴 = (𝑂 ∖ ∪ 𝑥 ∈ 𝐴 (𝑂 ∖ 𝑥))))
Theorem	iundifdif 32553*	The intersection of a set is the complement of the union of the complements. TODO: shorten using iundifdifd 32552. (Contributed by Thierry Arnoux, 4-Sep-2016.)
⊢ 𝑂 ∈ V    &   ⊢ 𝐴 ⊆ 𝒫 𝑂    ⇒   ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 = (𝑂 ∖ ∪ 𝑥 ∈ 𝐴 (𝑂 ∖ 𝑥)))
Theorem	iunrdx 32554*	Re-index an indexed union. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ (𝜑 → 𝐹:𝐴–onto→𝐶)    &   ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷)
Theorem	iunpreima 32555*	Preimage of an indexed union. (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ (Fun 𝐹 → (◡𝐹 “ ∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵))
Theorem	iunrnmptss 32556*	A subset relation for an indexed union over the range of function expressed as a mapping. (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∪ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐷)
Theorem	iunxunsn 32557*	Appending a set to an indexed union. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ∪ 𝑥 ∈ (𝐴 ∪ {𝑋})𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶))
Theorem	iunxunpr 32558*	Appending two sets to an indexed union. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ∪ 𝑥 ∈ (𝐴 ∪ {𝑋, 𝑌})𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ (𝐶 ∪ 𝐷)))
Theorem	iunxpssiun1 32559*	Provide an upper bound for the indexed union of cartesian products. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ⊆ 𝐸)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 × 𝐶) ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 × 𝐸))
21.3.3.9  Indexed intersection - misc additions
Theorem	iinabrex 32560*	Rewriting an indexed intersection into an intersection of its image set. (Contributed by Thierry Arnoux, 15-Jun-2024.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
21.3.3.10  Disjointness - misc additions
Theorem	disjnf 32561*	In case 𝑥 is not free in 𝐵, disjointness is not so interesting since it reduces to cases where 𝐴 is a singleton. (Google Groups discussion with Peter Mazsa.) (Contributed by Thierry Arnoux, 26-Jul-2018.)
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ (𝐵 = ∅ ∨ ∃*𝑥 𝑥 ∈ 𝐴))
Theorem	cbvdisjf 32562*	Change bound variables in a disjoint collection. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶)
Theorem	disjss1f 32563	A subset of a disjoint collection is disjoint. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶))
Theorem	disjeq1f 32564	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶))
Theorem	disjxun0 32565*	Simplify a disjoint union. (Contributed by Thierry Arnoux, 27-Nov-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = ∅)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ Disj 𝑥 ∈ 𝐴 𝐶))
Theorem	disjdifprg 32566*	A trivial partition into a subset and its complement. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Disj 𝑥 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑥)
Theorem	disjdifprg2 32567*	A trivial partition of a set into its difference and intersection with another set. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → Disj 𝑥 ∈ {(𝐴 ∖ 𝐵), (𝐴 ∩ 𝐵)}𝑥)
Theorem	disji2f 32568*	Property of a disjoint collection: if 𝐵(𝑥) = 𝐶 and 𝐵(𝑌) = 𝐷, and 𝑥 ≠ 𝑌, then 𝐵 and 𝐶 are disjoint. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶)    ⇒   ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑥 ≠ 𝑌) → (𝐵 ∩ 𝐶) = ∅)
Theorem	disjif 32569*	Property of a disjoint collection: if 𝐵(𝑥) and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑥 = 𝑌. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶)    ⇒   ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝑥 = 𝑌)
Theorem	disjorf 32570*	Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑖𝐴    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ (𝑖 = 𝑗 → 𝐵 = 𝐶)    ⇒   ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅))
Theorem	disjorsf 32571*	Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
Theorem	disjif2 32572*	Property of a disjoint collection: if 𝐵(𝑥) and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑥 = 𝑌. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶)    ⇒   ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝑥 = 𝑌)
Theorem	disjabrex 32573*	Rewriting a disjoint collection into a partition of its image set. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦)
Theorem	disjabrexf 32574*	Rewriting a disjoint collection into a partition of its image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) (Revised by Thierry Arnoux, 9-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦)
Theorem	disjpreima 32575*	A preimage of a disjoint set is disjoint. (Contributed by Thierry Arnoux, 7-Feb-2017.)
⊢ ((Fun 𝐹 ∧ Disj 𝑥 ∈ 𝐴 𝐵) → Disj 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵))
Theorem	disjrnmpt 32576*	Rewriting a disjoint collection using the range of a mapping. (Contributed by Thierry Arnoux, 27-May-2020.)
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦)
Theorem	disjin 32577	If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 14-Feb-2017.)
⊢ (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐵 (𝐶 ∩ 𝐴))
Theorem	disjin2 32578	If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐵 (𝐴 ∩ 𝐶))
Theorem	disjxpin 32579*	Derive a disjunction over a Cartesian product from the disjunctions over its first and second elements. (Contributed by Thierry Arnoux, 9-Mar-2018.)
⊢ (𝑥 = (1st ‘𝑝) → 𝐶 = 𝐸)    &   ⊢ (𝑦 = (2nd ‘𝑝) → 𝐷 = 𝐹)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐶)    &   ⊢ (𝜑 → Disj 𝑦 ∈ 𝐵 𝐷)    ⇒   ⊢ (𝜑 → Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹))
Theorem	iundisjf 32580*	Rewrite a countable union as a disjoint union. Cf. iundisj 25486. (Contributed by Thierry Arnoux, 31-Dec-2016.)
⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑛𝐵    &   ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    ⇒   ⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)
Theorem	iundisj2f 32581*	A disjoint union is disjoint. Cf. iundisj2 25487. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑛𝐵    &   ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    ⇒   ⊢ Disj 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)
Theorem	disjrdx 32582*	Re-index a disjunct collection statement. (Contributed by Thierry Arnoux, 7-Apr-2017.)
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐶)    &   ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐶 𝐷))
Theorem	disjex 32583*	Two ways to say that two classes are disjoint (or equal). (Contributed by Thierry Arnoux, 4-Oct-2016.)
⊢ ((∃𝑧(𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝐴 = 𝐵) ↔ (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅))
Theorem	disjexc 32584*	A variant of disjex 32583, applicable for more generic families. (Contributed by Thierry Arnoux, 4-Oct-2016.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ((∃𝑧(𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝑥 = 𝑦) → (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅))
Theorem	disjunsn 32585*	Append an element to a disjoint collection. Similar to ralunsn 4847, gsumunsn 19882, etc. (Contributed by Thierry Arnoux, 28-Mar-2018.)
⊢ (𝑥 = 𝑀 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
Theorem	disjun0 32586*	Adding the empty element preserves disjointness. (Contributed by Thierry Arnoux, 30-May-2020.)
⊢ (Disj 𝑥 ∈ 𝐴 𝑥 → Disj 𝑥 ∈ (𝐴 ∪ {∅})𝑥)
Theorem	disjiunel 32587*	A set of elements B of a disjoint set A is disjoint with another element of that set. (Contributed by Thierry Arnoux, 24-May-2020.)
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐸 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴 ∖ 𝐸))    ⇒   ⊢ (𝜑 → (∪ 𝑥 ∈ 𝐸 𝐵 ∩ 𝐷) = ∅)
Theorem	disjuniel 32588*	A set of elements B of a disjoint set A is disjoint with another element of that set. (Contributed by Thierry Arnoux, 24-May-2020.)
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵))    ⇒   ⊢ (𝜑 → (∪ 𝐵 ∩ 𝐶) = ∅)
21.3.4  Relations and Functions
21.3.4.1  Relations - misc additions
Theorem	xpdisjres 32589	Restriction of a constant function (or other Cartesian product) outside of its domain. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) ↾ 𝐶) = ∅)
Theorem	opeldifid 32590	Ordered pair elementhood outside of the diagonal. (Contributed by Thierry Arnoux, 1-Jan-2020.)
⊢ (Rel 𝐴 → (⟨𝑋, 𝑌⟩ ∈ (𝐴 ∖ I ) ↔ (⟨𝑋, 𝑌⟩ ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)))
Theorem	difres 32591	Case when class difference in unaffected by restriction. (Contributed by Thierry Arnoux, 1-Jan-2020.)
⊢ (𝐴 ⊆ (𝐵 × V) → (𝐴 ∖ (𝐶 ↾ 𝐵)) = (𝐴 ∖ 𝐶))
Theorem	imadifxp 32592	Image of the difference with a Cartesian product. (Contributed by Thierry Arnoux, 13-Dec-2017.)
⊢ (𝐶 ⊆ 𝐴 → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
Theorem	relfi 32593	A relation (set) is finite if and only if both its domain and range are finite. (Contributed by Thierry Arnoux, 27-Aug-2017.)
⊢ (Rel 𝐴 → (𝐴 ∈ Fin ↔ (dom 𝐴 ∈ Fin ∧ ran 𝐴 ∈ Fin)))
Theorem	0res 32594	Restriction of the empty function. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ (∅ ↾ 𝐴) = ∅
Theorem	fcoinver 32595	Build an equivalence relation from a function. Two values are equivalent if they have the same image by the function. See also fcoinvbr 32596. (Contributed by Thierry Arnoux, 3-Jan-2020.)
⊢ (𝐹 Fn 𝑋 → (◡𝐹 ∘ 𝐹) Er 𝑋)
Theorem	fcoinvbr 32596	Binary relation for the equivalence relation from fcoinver 32595. (Contributed by Thierry Arnoux, 3-Jan-2020.)
⊢ ∼ = (◡𝐹 ∘ 𝐹)    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∼ 𝑌 ↔ (𝐹‘𝑋) = (𝐹‘𝑌)))
Theorem	breq1dd 32597	Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐵𝑅𝐶)
Theorem	breq2dd 32598	Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶𝑅𝐴)    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐵)
Theorem	brab2d 32599*	Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑉) ∧ 𝜓)})    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ 𝜒)))
Theorem	brabgaf 32600*	The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) (Revised by Thierry Arnoux, 17-May-2020.)
⊢ Ⅎ𝑥𝜓    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓))