Theorem elun 3314

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 2783	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2783	. . 3 |- ( A e. B -> A e. _V )
3		elex 2783	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 718	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2268	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2268	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 795	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3170	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2920	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 706	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 105   \/ wo 710   = wceq 1373   e. wcel 2176   _Vcvv 2772   u. cun 3164

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170

This theorem is referenced by:  uneqri  3315  uncom  3317  uneq1  3320  unass  3330  ssun1  3336  unss1  3342  ssequn1  3343  unss  3347  rexun  3353  ralunb  3354  unssdif  3408  unssin  3412  inssun  3413  indi  3420  undi  3421  difundi  3425  difindiss  3427  undif3ss  3434  symdifxor  3439  rabun2  3452  reuun2  3456  undif4  3523  ssundifim  3544  dcun  3570  dfpr2  3652  eltpg  3678  pwprss  3846  pwtpss  3847  uniun  3869  intun  3916  iunun  4006  iunxun  4007  iinuniss  4010  brun  4095  undifexmid  4237  exmidundif  4250  exmidundifim  4251  exmid1stab  4252  pwunss  4330  elsuci  4450  elsucg  4451  elsuc2g  4452  ordsucim  4548  sucprcreg  4597  opthprc  4726  xpundi  4731  xpundir  4732  funun  5315  mptun  5407  unpreima  5705  reldmtpos  6339  dftpos4  6349  tpostpos  6350  onunsnss  7014  unfidisj  7019  undifdcss  7020  fidcenumlemrks  7055  djulclb  7157  eldju  7170  eldju2ndl  7174  eldju2ndr  7175  ctssdccl  7213  pw1nel3  7343  sucpw1nel3  7345  elnn0  9297  un0addcl  9328  un0mulcl  9329  elxnn0  9360  ltxr  9897  elxr  9898  fzsplit2  10172  elfzp1  10194  uzsplit  10214  elfzp12  10221  fz01or  10233  fzosplit  10301  fzouzsplit  10303  elfzonlteqm1  10339  fzosplitsni  10364  hashinfuni  10922  hashennnuni  10924  hashunlem  10949  zfz1isolemiso  10984  ccatrn  11065  summodclem3  11691  fsumsplit  11718  fsumsplitsn  11721  sumsplitdc  11743  fprodsplitdc  11907  fprodsplit  11908  fprodunsn  11915  fprodsplitsn  11944  nnnn0modprm0  12578  prm23lt5  12586  reopnap  15018  plyaddlem1  15219  plymullem1  15220  plycoeid3  15229  plycj  15233  lgsdir2  15510  2lgslem3  15578  2lgsoddprmlem3  15588  djulclALT  15737  djurclALT  15738  bj-charfun  15743  bj-nntrans  15887  bj-nnelirr  15889