Theorem cbviunv

Description: 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 . See cbviunvg for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024)

	Ref	Expression
Hypothesis	cbviunv.1	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
Assertion	cbviunv	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Proof

Step	Hyp	Ref	Expression
1		cbviunv.1	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
2		nfcv	⊢ Ⅎ 𝑦 𝐵
3		nfcv	⊢ Ⅎ 𝑥 𝐶
4	2 3 1	cbviun	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶