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

Metamath Proof Explorer

Theorem iunab

Description: The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ y A
2 nfab1 
 |-  F/_ y { y | ph }
3 1 2 nfiun 
 |-  F/_ y U_ x e. A { y | ph }
4 nfab1 
 |-  F/_ y { y | E. x e. A ph }
5 abid 
 |-  ( y e. { y | ph } <-> ph )
6 5 rexbii 
 |-  ( E. x e. A y e. { y | ph } <-> E. x e. A ph )
7 eliun 
 |-  ( y e. U_ x e. A { y | ph } <-> E. x e. A y e. { y | ph } )
8 abid 
 |-  ( y e. { y | E. x e. A ph } <-> E. x e. A ph )
9 6 7 8 3bitr4i 
 |-  ( y e. U_ x e. A { y | ph } <-> y e. { y | E. x e. A ph } )
10 3 4 9 eqri 
 |-  U_ x e. A { y | ph } = { y | E. x e. A ph }