Theorem cbviuneq12dv

Description: Rule used to change the bound variables and classes in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by RP, 17-Jul-2020)

	Ref	Expression
Hypotheses	cbviuneq12dv.xel	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝑋 ∈ 𝐴 )
	cbviuneq12dv.yel	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐶 )
	cbviuneq12dv.xsub	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝑋 ) → 𝐵 = 𝐹 )
	cbviuneq12dv.ysub	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌 ) → 𝐷 = 𝐺 )
	cbviuneq12dv.eq1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐺 )
	cbviuneq12dv.eq2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐷 = 𝐹 )
Assertion	cbviuneq12dv	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		cbviuneq12dv.xel	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝑋 ∈ 𝐴 )
2		cbviuneq12dv.yel	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐶 )
3		cbviuneq12dv.xsub	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝑋 ) → 𝐵 = 𝐹 )
4		cbviuneq12dv.ysub	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌 ) → 𝐷 = 𝐺 )
5		cbviuneq12dv.eq1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐺 )
6		cbviuneq12dv.eq2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐷 = 𝐹 )
7		nfv	⊢ Ⅎ 𝑥 𝜑
8		nfv	⊢ Ⅎ 𝑦 𝜑
9		nfcv	⊢ Ⅎ 𝑥 𝑋
10		nfcv	⊢ Ⅎ 𝑦 𝑌
11		nfcv	⊢ Ⅎ 𝑥 𝐴
12		nfcv	⊢ Ⅎ 𝑦 𝐴
13		nfcv	⊢ Ⅎ 𝑦 𝐵
14		nfcv	⊢ Ⅎ 𝑥 𝐶
15		nfcv	⊢ Ⅎ 𝑦 𝐶
16		nfcv	⊢ Ⅎ 𝑥 𝐷
17		nfcv	⊢ Ⅎ 𝑥 𝐹
18		nfcv	⊢ Ⅎ 𝑦 𝐺
19	7 8 9 10 11 12 13 14 15 16 17 18 1 2 3 4 5 6	cbviuneq12df	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷 )