Theorem elun 3318

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 2785	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2785	. . 3 |- ( A e. B -> A e. _V )
3		elex 2785	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 718	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2269	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2269	. . . 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 3174	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2924	. 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 2177   _Vcvv 2773   u. cun 3168

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174

This theorem is referenced by:  uneqri  3319  uncom  3321  uneq1  3324  unass  3334  ssun1  3340  unss1  3346  ssequn1  3347  unss  3351  rexun  3357  ralunb  3358  unssdif  3412  unssin  3416  inssun  3417  indi  3424  undi  3425  difundi  3429  difindiss  3431  undif3ss  3438  symdifxor  3443  rabun2  3456  reuun2  3460  undif4  3527  ssundifim  3548  dcun  3574  dfpr2  3657  eltpg  3683  pwprss  3855  pwtpss  3856  uniun  3878  intun  3925  iunun  4015  iunxun  4016  iinuniss  4019  brun  4106  undifexmid  4248  exmidundif  4261  exmidundifim  4262  exmid1stab  4263  pwunss  4343  elsuci  4463  elsucg  4464  elsuc2g  4465  ordsucim  4561  sucprcreg  4610  opthprc  4739  xpundi  4744  xpundir  4745  funun  5329  mptun  5422  unpreima  5723  reldmtpos  6357  dftpos4  6367  tpostpos  6368  onunsnss  7035  unfidisj  7040  undifdcss  7041  fidcenumlemrks  7076  djulclb  7178  eldju  7191  eldju2ndl  7195  eldju2ndr  7196  ctssdccl  7234  pw1nel3  7372  sucpw1nel3  7374  elnn0  9327  un0addcl  9358  un0mulcl  9359  elxnn0  9390  ltxr  9927  elxr  9928  fzsplit2  10202  elfzp1  10224  uzsplit  10244  elfzp12  10251  fz01or  10263  fzosplit  10331  fzouzsplit  10333  elfzonlteqm1  10371  fzosplitsni  10396  hashinfuni  10954  hashennnuni  10956  hashunlem  10981  zfz1isolemiso  11016  ccatrn  11098  cats1un  11207  summodclem3  11776  fsumsplit  11803  fsumsplitsn  11806  sumsplitdc  11828  fprodsplitdc  11992  fprodsplit  11993  fprodunsn  12000  fprodsplitsn  12029  nnnn0modprm0  12663  prm23lt5  12671  reopnap  15103  plyaddlem1  15304  plymullem1  15305  plycoeid3  15314  plycj  15318  lgsdir2  15595  2lgslem3  15663  2lgsoddprmlem3  15673  djulclALT  15907  djurclALT  15908  bj-charfun  15912  bj-nntrans  16056  bj-nnelirr  16058