Theorem elun 3301

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 2771	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2771	. . 3 |- ( A e. B -> A e. _V )
3		elex 2771	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 717	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2256	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2256	. . . 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 3158	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2908	. 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 1364   e. wcel 2164   _Vcvv 2760   u. cun 3152

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158

This theorem is referenced by:  uneqri  3302  uncom  3304  uneq1  3307  unass  3317  ssun1  3323  unss1  3329  ssequn1  3330  unss  3334  rexun  3340  ralunb  3341  unssdif  3395  unssin  3399  inssun  3400  indi  3407  undi  3408  difundi  3412  difindiss  3414  undif3ss  3421  symdifxor  3426  rabun2  3439  reuun2  3443  undif4  3510  ssundifim  3531  dcun  3557  dfpr2  3638  eltpg  3664  pwprss  3832  pwtpss  3833  uniun  3855  intun  3902  iunun  3992  iunxun  3993  iinuniss  3996  brun  4081  undifexmid  4223  exmidundif  4236  exmidundifim  4237  exmid1stab  4238  pwunss  4315  elsuci  4435  elsucg  4436  elsuc2g  4437  ordsucim  4533  sucprcreg  4582  opthprc  4711  xpundi  4716  xpundir  4717  funun  5299  mptun  5386  unpreima  5684  reldmtpos  6308  dftpos4  6318  tpostpos  6319  onunsnss  6975  unfidisj  6980  undifdcss  6981  fidcenumlemrks  7014  djulclb  7116  eldju  7129  eldju2ndl  7133  eldju2ndr  7134  ctssdccl  7172  pw1nel3  7293  sucpw1nel3  7295  elnn0  9245  un0addcl  9276  un0mulcl  9277  elxnn0  9308  ltxr  9844  elxr  9845  fzsplit2  10119  elfzp1  10141  uzsplit  10161  elfzp12  10168  fz01or  10180  fzosplit  10247  fzouzsplit  10249  elfzonlteqm1  10280  fzosplitsni  10305  hashinfuni  10851  hashennnuni  10853  hashunlem  10878  zfz1isolemiso  10913  summodclem3  11526  fsumsplit  11553  fsumsplitsn  11556  sumsplitdc  11578  fprodsplitdc  11742  fprodsplit  11743  fprodunsn  11750  fprodsplitsn  11779  nnnn0modprm0  12396  prm23lt5  12404  reopnap  14725  plyaddlem1  14926  plymullem1  14927  plycj  14939  lgsdir2  15190  2lgslem3  15258  2lgsoddprmlem3  15268  djulclALT  15363  djurclALT  15364  bj-charfun  15369  bj-nntrans  15513  bj-nnelirr  15515