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 = A -> ( x e. B <-> A e. B ) )
6		eleq1	|- ( x = A -> ( x e. C <-> A e. C ) )
7	5 6	orbi12d	|- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un	|- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7 8	elab2g	|- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1 4 9	pm5.21nii	|- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )