Metamath Proof Explorer


Theorem iuneq12df

Description: Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 31-Dec-2016)

Ref Expression
Hypotheses iuneq12df.1 xφ
iuneq12df.2 _xA
iuneq12df.3 _xB
iuneq12df.4 φA=B
iuneq12df.5 φC=D
Assertion iuneq12df φxAC=xBD

Proof

Step Hyp Ref Expression
1 iuneq12df.1 xφ
2 iuneq12df.2 _xA
3 iuneq12df.3 _xB
4 iuneq12df.4 φA=B
5 iuneq12df.5 φC=D
6 5 eleq2d φyCyD
7 1 2 3 4 6 rexeqbid φxAyCxByD
8 7 alrimiv φyxAyCxByD
9 abbi yxAyCxByDy|xAyC=y|xByD
10 df-iun xAC=y|xAyC
11 df-iun xBD=y|xByD
12 9 10 11 3eqtr4g yxAyCxByDxAC=xBD
13 8 12 syl φxAC=xBD