Theorem elun 3276

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

Assertion

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

Proof of Theorem elun

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2748	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2748	. . 3 |- ( A e. B -> A e. _V )
3		elex 2748	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 716	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2240	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2240	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 793	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3133	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2884	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 704	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 105   \/ wo 708   = wceq 1353   e. wcel 2148   _Vcvv 2737   u. cun 3127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133

This theorem is referenced by:  uneqri  3277  uncom  3279  uneq1  3282  unass  3292  ssun1  3298  unss1  3304  ssequn1  3305  unss  3309  rexun  3315  ralunb  3316  unssdif  3370  unssin  3374  inssun  3375  indi  3382  undi  3383  difundi  3387  difindiss  3389  undif3ss  3396  symdifxor  3401  rabun2  3414  reuun2  3418  undif4  3485  ssundifim  3506  dcun  3533  dfpr2  3611  eltpg  3637  pwprss  3805  pwtpss  3806  uniun  3828  intun  3875  iunun  3965  iunxun  3966  iinuniss  3969  brun  4054  undifexmid  4193  exmidundif  4206  exmidundifim  4207  exmid1stab  4208  pwunss  4283  elsuci  4403  elsucg  4404  elsuc2g  4405  ordsucim  4499  sucprcreg  4548  opthprc  4677  xpundi  4682  xpundir  4683  funun  5260  mptun  5347  unpreima  5641  reldmtpos  6253  dftpos4  6263  tpostpos  6264  onunsnss  6915  unfidisj  6920  undifdcss  6921  fidcenumlemrks  6951  djulclb  7053  eldju  7066  eldju2ndl  7070  eldju2ndr  7071  ctssdccl  7109  pw1nel3  7229  sucpw1nel3  7231  elnn0  9177  un0addcl  9208  un0mulcl  9209  elxnn0  9240  ltxr  9774  elxr  9775  fzsplit2  10049  elfzp1  10071  uzsplit  10091  elfzp12  10098  fz01or  10110  fzosplit  10176  fzouzsplit  10178  elfzonlteqm1  10209  fzosplitsni  10234  hashinfuni  10756  hashennnuni  10758  hashunlem  10783  zfz1isolemiso  10818  summodclem3  11387  fsumsplit  11414  fsumsplitsn  11417  sumsplitdc  11439  fprodsplitdc  11603  fprodsplit  11604  fprodunsn  11611  fprodsplitsn  11640  nnnn0modprm0  12254  prm23lt5  12262  reopnap  14008  lgsdir2  14404  2lgsoddprmlem3  14429  djulclALT  14523  djurclALT  14524  bj-charfun  14529  bj-nntrans  14673  bj-nnelirr  14675