Theorem cbviuneq12df

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	cbviuneq12df.xph	⊢ Ⅎ 𝑥 𝜑
	cbviuneq12df.yph	⊢ Ⅎ 𝑦 𝜑
	cbviuneq12df.x	⊢ Ⅎ 𝑥 𝑋
	cbviuneq12df.y	⊢ Ⅎ 𝑦 𝑌
	cbviuneq12df.xa	⊢ Ⅎ 𝑥 𝐴
	cbviuneq12df.ya	⊢ Ⅎ 𝑦 𝐴
	cbviuneq12df.b	⊢ Ⅎ 𝑦 𝐵
	cbviuneq12df.xc	⊢ Ⅎ 𝑥 𝐶
	cbviuneq12df.yc	⊢ Ⅎ 𝑦 𝐶
	cbviuneq12df.d	⊢ Ⅎ 𝑥 𝐷
	cbviuneq12df.f	⊢ Ⅎ 𝑥 𝐹
	cbviuneq12df.g	⊢ Ⅎ 𝑦 𝐺
	cbviuneq12df.xel	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝑋 ∈ 𝐴 )
	cbviuneq12df.yel	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐶 )
	cbviuneq12df.xsub	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝑋 ) → 𝐵 = 𝐹 )
	cbviuneq12df.ysub	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌 ) → 𝐷 = 𝐺 )
	cbviuneq12df.eq1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐺 )
	cbviuneq12df.eq2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐷 = 𝐹 )
Assertion	cbviuneq12df	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		cbviuneq12df.xph	⊢ Ⅎ 𝑥 𝜑
2		cbviuneq12df.yph	⊢ Ⅎ 𝑦 𝜑
3		cbviuneq12df.x	⊢ Ⅎ 𝑥 𝑋
4		cbviuneq12df.y	⊢ Ⅎ 𝑦 𝑌
5		cbviuneq12df.xa	⊢ Ⅎ 𝑥 𝐴
6		cbviuneq12df.ya	⊢ Ⅎ 𝑦 𝐴
7		cbviuneq12df.b	⊢ Ⅎ 𝑦 𝐵
8		cbviuneq12df.xc	⊢ Ⅎ 𝑥 𝐶
9		cbviuneq12df.yc	⊢ Ⅎ 𝑦 𝐶
10		cbviuneq12df.d	⊢ Ⅎ 𝑥 𝐷
11		cbviuneq12df.f	⊢ Ⅎ 𝑥 𝐹
12		cbviuneq12df.g	⊢ Ⅎ 𝑦 𝐺
13		cbviuneq12df.xel	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝑋 ∈ 𝐴 )
14		cbviuneq12df.yel	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐶 )
15		cbviuneq12df.xsub	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝑋 ) → 𝐵 = 𝐹 )
16		cbviuneq12df.ysub	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌 ) → 𝐷 = 𝐺 )
17		cbviuneq12df.eq1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐺 )
18		cbviuneq12df.eq2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐷 = 𝐹 )
19		eqimss	⊢ ( 𝐵 = 𝐺 → 𝐵 ⊆ 𝐺 )
20	17 19	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐺 )
21	1 2 4 6 7 8 9 10 12 14 16 20	ss2iundf	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )
22		eqimss	⊢ ( 𝐷 = 𝐹 → 𝐷 ⊆ 𝐹 )
23	18 22	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐷 ⊆ 𝐹 )
24	2 1 3 8 10 6 5 7 11 13 15 23	ss2iundf	⊢ ( 𝜑 → ∪ 𝑦 ∈ 𝐶 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
25	21 24	eqssd	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷 )