Theorem elun 3364

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 2827	. 2 |- ( A e. ( B u. C ) -> A e. _V )
2		elex 2827	. . 3 |- ( A e. B -> A e. _V )
3		elex 2827	. . 3 |- ( A e. C -> A e. _V )
4	2, 3	jaoi 724	. 2 |- ( ( A e. B \/ A e. C ) -> A e. _V )
5		eleq1 2297	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
6		eleq1 2297	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
7	5, 6	orbi12d 801	. . 3 |- ( x = A -> ( ( x e. B \/ x e. C ) <-> ( A e. B \/ A e. C ) ) )
8		df-un 3218	. . 3 |- ( B u. C ) = { x | ( x e. B \/ x e. C ) }
9	7, 8	elab2g 2967	. 2 |- ( A e. _V -> ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) ) )
10	1, 4, 9	pm5.21nii 712	1 |- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )

Syntax hints:   <-> wb 105   \/ wo 716   = wceq 1398   e. wcel 2205   _Vcvv 2815   u. cun 3212

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218

This theorem is referenced by:  uneqri  3365  uncom  3367  uneq1  3370  unass  3380  ssun1  3386  unss1  3392  ssequn1  3393  unss  3397  rexun  3403  ralunb  3404  unssdif  3460  unssin  3464  inssun  3465  indi  3472  undi  3473  difundi  3477  difindiss  3479  undif3ss  3486  symdifxor  3491  rabun2  3504  reuun2  3508  undif4  3575  ssundifim  3597  dcun  3623  dfpr2  3713  eltpg  3739  pwprss  3915  pwtpss  3916  uniun  3938  intun  3985  iunun  4075  iunxun  4076  iinuniss  4079  brun  4166  undifexmid  4311  exmidundif  4324  exmidundifim  4325  exmid1stab  4326  pwunss  4409  elsuci  4529  elsucg  4530  elsuc2g  4531  ordsucim  4627  sucprcreg  4676  opthprc  4806  xpundi  4811  xpundir  4812  funun  5402  mptun  5495  unpreima  5807  reldmtpos  6497  dftpos4  6507  tpostpos  6508  elssdc  7175  onunsnss  7190  unfidisj  7195  undifdcss  7196  fidcenumlemrks  7236  djulclb  7359  eldju  7372  eldju2ndl  7376  eldju2ndr  7377  ctssdccl  7415  pw1nel3  7554  sucpw1nel3  7556  elnn0  9515  un0addcl  9546  un0mulcl  9547  elxnn0  9582  ltxr  10127  elxr  10128  fzsplit2  10404  fzsplit3  10407  elfzp1  10428  uzsplit  10448  elfzp12  10455  fz01or  10467  fzosplit  10535  fzouzsplit  10537  elfzonlteqm1  10577  fzosplitsni  10603  hashinfuni  11165  hashennnuni  11167  hashunlem  11193  zfz1isolemiso  11236  ccatrn  11322  cats1un  11438  summodclem3  12091  fsumsplit  12118  fsumsplitsn  12121  sumsplitdc  12143  fprodsplitdc  12307  fprodsplit  12308  fprodunsn  12315  fprodsplitsn  12344  nnnn0modprm0  12978  prm23lt5  12986  reopnap  15537  plyaddlem1  15738  plymullem1  15739  plycoeid3  15748  plycj  15752  lgsdir2  16032  2lgslem3  16100  2lgsoddprmlem3  16110  vtxdfifiun  16418  djulclALT  16699  djurclALT  16700  bj-charfun  16703  bj-nntrans  16847  bj-nnelirr  16849