This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iunrab

Description: The indexed union of a restricted class abstraction. (Contributed by NM, 3-Jan-2004) (Proof shortened by Mario Carneiro, 14-Nov-2016)

Ref Expression
Assertion iunrab 
|- U_ x e. A { y e. B | ph } = { y e. B | E. x e. A ph }

Proof

Step Hyp Ref Expression
1 iunab 
 |-  U_ x e. A { y | ( y e. B /\ ph ) } = { y | E. x e. A ( y e. B /\ ph ) }
2 df-rab 
 |-  { y e. B | ph } = { y | ( y e. B /\ ph ) }
3 2 a1i 
 |-  ( x e. A -> { y e. B | ph } = { y | ( y e. B /\ ph ) } )
4 3 iuneq2i 
 |-  U_ x e. A { y e. B | ph } = U_ x e. A { y | ( y e. B /\ ph ) }
5 df-rab 
 |-  { y e. B | E. x e. A ph } = { y | ( y e. B /\ E. x e. A ph ) }
6 r19.42v 
 |-  ( E. x e. A ( y e. B /\ ph ) <-> ( y e. B /\ E. x e. A ph ) )
7 6 abbii 
 |-  { y | E. x e. A ( y e. B /\ ph ) } = { y | ( y e. B /\ E. x e. A ph ) }
8 5 7 eqtr4i 
 |-  { y e. B | E. x e. A ph } = { y | E. x e. A ( y e. B /\ ph ) }
9 1 4 8 3eqtr4i 
 |-  U_ x e. A { y e. B | ph } = { y e. B | E. x e. A ph }