Metamath Proof Explorer

Theorem elun

Description: Expansion of membership in class union. Theorem 12 of Suppes p. 25. (Contributed by NM, 7-Aug-1994)

Ref Expression
Assertion elun 
|- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. ( B u. C ) -> A e. _V )
2 elex 
 |-  ( A e. B -> A e. _V )
3 elex 
 |-  ( A e. C -> A e. _V )
4 2 3 jaoi 
 |-  ( ( A e. B \/ A e. C ) -> A e. _V )
5 eleq1 
 |-  ( x = y -> ( x e. B <-> y e. B ) )
6 eleq1 
 |-  ( x = y -> ( x e. C <-> y e. C ) )
7 5 6 orbi12d 
 |-  ( x = y -> ( ( x e. B \/ x e. C ) <-> ( y e. B \/ y e. C ) ) )
8 eleq1 
 |-  ( y = A -> ( y e. B <-> A e. B ) )
9 eleq1 
 |-  ( y = A -> ( y e. C <-> A e. C ) )
10 8 9 orbi12d 
 |-  ( y = A -> ( ( y e. B \/ y e. C ) <-> ( A e. B \/ A e. C ) ) )
11 df-un 
 |-  ( B u. C ) = { x | ( x e. B \/ x e. C ) }
12 7 10 11 elab2gw 
 |-  ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
13 1 4 12 pm5.21nii 
 |-  ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )