Theorem elun 3313

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 2782	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2782	. . 3 |- ( A e. B -> A e. _V )
3		elex 2782	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 717	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2267	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2267	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 794	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3169	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2919	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 705	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 105   \/ wo 709   = wceq 1372   e. wcel 2175   _Vcvv 2771   u. cun 3163

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169

This theorem is referenced by:  uneqri  3314  uncom  3316  uneq1  3319  unass  3329  ssun1  3335  unss1  3341  ssequn1  3342  unss  3346  rexun  3352  ralunb  3353  unssdif  3407  unssin  3411  inssun  3412  indi  3419  undi  3420  difundi  3424  difindiss  3426  undif3ss  3433  symdifxor  3438  rabun2  3451  reuun2  3455  undif4  3522  ssundifim  3543  dcun  3569  dfpr2  3651  eltpg  3677  pwprss  3845  pwtpss  3846  uniun  3868  intun  3915  iunun  4005  iunxun  4006  iinuniss  4009  brun  4094  undifexmid  4236  exmidundif  4249  exmidundifim  4250  exmid1stab  4251  pwunss  4329  elsuci  4449  elsucg  4450  elsuc2g  4451  ordsucim  4547  sucprcreg  4596  opthprc  4725  xpundi  4730  xpundir  4731  funun  5314  mptun  5406  unpreima  5704  reldmtpos  6338  dftpos4  6348  tpostpos  6349  onunsnss  7013  unfidisj  7018  undifdcss  7019  fidcenumlemrks  7054  djulclb  7156  eldju  7169  eldju2ndl  7173  eldju2ndr  7174  ctssdccl  7212  pw1nel3  7342  sucpw1nel3  7344  elnn0  9296  un0addcl  9327  un0mulcl  9328  elxnn0  9359  ltxr  9896  elxr  9897  fzsplit2  10171  elfzp1  10193  uzsplit  10213  elfzp12  10220  fz01or  10232  fzosplit  10299  fzouzsplit  10301  elfzonlteqm1  10337  fzosplitsni  10362  hashinfuni  10920  hashennnuni  10922  hashunlem  10947  zfz1isolemiso  10982  ccatrn  11063  summodclem3  11633  fsumsplit  11660  fsumsplitsn  11663  sumsplitdc  11685  fprodsplitdc  11849  fprodsplit  11850  fprodunsn  11857  fprodsplitsn  11886  nnnn0modprm0  12520  prm23lt5  12528  reopnap  14960  plyaddlem1  15161  plymullem1  15162  plycoeid3  15171  plycj  15175  lgsdir2  15452  2lgslem3  15520  2lgsoddprmlem3  15530  djulclALT  15670  djurclALT  15671  bj-charfun  15676  bj-nntrans  15820  bj-nnelirr  15822