Metamath Proof Explorer

Theorem eluni2

Description: Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999)

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

Proof

Step Hyp Ref Expression
1 exancom 
 |-  ( E. x ( A e. x /\ x e. B ) <-> E. x ( x e. B /\ A e. x ) )
2 eluni 
 |-  ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )
3 df-rex 
 |-  ( E. x e. B A e. x <-> E. x ( x e. B /\ A e. x ) )
4 1 2 3 3bitr4i 
 |-  ( A e. U. B <-> E. x e. B A e. x )