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	|- ( ( ph /\ y e. C ) -> X e. A )
	cbviuneq12dv.yel	|- ( ( ph /\ x e. A ) -> Y e. C )
	cbviuneq12dv.xsub	|- ( ( ph /\ y e. C /\ x = X ) -> B = F )
	cbviuneq12dv.ysub	|- ( ( ph /\ x e. A /\ y = Y ) -> D = G )
	cbviuneq12dv.eq1	|- ( ( ph /\ x e. A ) -> B = G )
	cbviuneq12dv.eq2	|- ( ( ph /\ y e. C ) -> D = F )
Assertion	cbviuneq12dv	|- ( ph -> U_ x e. A B = U_ y e. C D )

Proof

Step	Hyp	Ref	Expression
1		cbviuneq12dv.xel	|- ( ( ph /\ y e. C ) -> X e. A )
2		cbviuneq12dv.yel	|- ( ( ph /\ x e. A ) -> Y e. C )
3		cbviuneq12dv.xsub	|- ( ( ph /\ y e. C /\ x = X ) -> B = F )
4		cbviuneq12dv.ysub	|- ( ( ph /\ x e. A /\ y = Y ) -> D = G )
5		cbviuneq12dv.eq1	|- ( ( ph /\ x e. A ) -> B = G )
6		cbviuneq12dv.eq2	|- ( ( ph /\ y e. C ) -> D = F )
7		nfv	|- F/ x ph
8		nfv	|- F/ y ph
9		nfcv	|- F/_ x X
10		nfcv	|- F/_ y Y
11		nfcv	|- F/_ x A
12		nfcv	|- F/_ y A
13		nfcv	|- F/_ y B
14		nfcv	|- F/_ x C
15		nfcv	|- F/_ y C
16		nfcv	|- F/_ x D
17		nfcv	|- F/_ x F
18		nfcv	|- F/_ y G
19	7 8 9 10 11 12 13 14 15 16 17 18 1 2 3 4 5 6	cbviuneq12df	|- ( ph -> U_ x e. A B = U_ y e. C D )