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

Metamath Proof Explorer

Theorem eluni

Description: Membership in class union. (Contributed by NM, 22-May-1994)

Ref Expression
Assertion eluni 
|- ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. U. B -> A e. _V )
2 elex 
 |-  ( A e. x -> A e. _V )
3 2 adantr 
 |-  ( ( A e. x /\ x e. B ) -> A e. _V )
4 3 exlimiv 
 |-  ( E. x ( A e. x /\ x e. B ) -> A e. _V )
5 eleq1 
 |-  ( y = A -> ( y e. x <-> A e. x ) )
6 5 anbi1d 
 |-  ( y = A -> ( ( y e. x /\ x e. B ) <-> ( A e. x /\ x e. B ) ) )
7 6 exbidv 
 |-  ( y = A -> ( E. x ( y e. x /\ x e. B ) <-> E. x ( A e. x /\ x e. B ) ) )
8 df-uni 
 |-  U. B = { y | E. x ( y e. x /\ x e. B ) }
9 7 8 elab2g 
 |-  ( A e. _V -> ( A e. U. B <-> E. x ( A e. x /\ x e. B ) ) )
10 1 4 9 pm5.21nii 
 |-  ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )