Metamath Proof Explorer


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 ( 𝜑 𝑥𝐴 𝐵 = 𝑦𝐶 𝐷 )