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 3 4 cleqf 
 |-  ( U_ x e. A { y | ph } = { y | E. x e. A ph } <-> A. y ( y e. U_ x e. A { y | ph } <-> y e. { y | E. x e. A ph } ) )
6 abid 
 |-  ( y e. { y | ph } <-> ph )
7 6 rexbii 
 |-  ( E. x e. A y e. { y | ph } <-> E. x e. A ph )
8 eliun 
 |-  ( y e. U_ x e. A { y | ph } <-> E. x e. A y e. { y | ph } )
9 abid 
 |-  ( y e. { y | E. x e. A ph } <-> E. x e. A ph )
10 7 8 9 3bitr4i 
 |-  ( y e. U_ x e. A { y | ph } <-> y e. { y | E. x e. A ph } )
11 5 10 mpgbir 
 |-  U_ x e. A { y | ph } = { y | E. x e. A ph }