Theorem elun 4102

Description: Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.)

Assertion

Ref	Expression
elun	⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Proof of Theorem elun

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3458	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3458	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3458	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 857	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2821	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2821	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 918	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3903	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3632	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1541   ∈ wcel 2113  Vcvv 3437   ∪ cun 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903

This theorem is referenced by:  elunnel1  4103  elunnel2  4104  uneqri  4105  uncom  4107  uneq1  4110  nfun  4119  unass  4121  ssun1  4127  elunant  4133  unss1  4134  ssequn1  4135  rexun  4145  elsymdif  4207  indi  4233  undi  4234  unineq  4237  undif3  4249  rabun2  4273  reuun2  4274  undif4  4416  ssundif  4437  dfpr2  4596  elunsn  4635  elpwunsn  4636  eltpg  4638  el7g  4642  pwpr  4852  pwtp  4853  uniun  4881  iinun2  5023  iunun  5043  iunxun  5044  iinuni  5048  brun  5144  pwssun  5511  opthprc  5683  xpundi  5688  xpundir  5689  imadifssran  6103  difxp  6116  sossfld  6138  elsuci  6380  elsucg  6381  elsuc2g  6382  funun  6532  mptun  6632  unima  6903  eqfnun  6976  unpreima  7002  ordsucun  7761  resf1extb  7870  fnse  8069  xpord2pred  8081  xpord3pred  8088  suppofssd  8139  reldmtpos  8170  dftpos4  8181  tpostpos  8182  frrlem12  8233  frrlem13  8234  oarec  8483  brdom2  8911  unfi  9087  unxpdomlem3  9149  domunfican  9213  dfsup2  9335  wemapso2lem  9445  unwdomg  9477  unxpwdom2  9481  cantnfp1lem3  9577  rankunb  9750  djur  9819  djuunxp  9821  eldju2ndl  9824  eldju2ndr  9825  djuun  9826  iscard3  9991  kmlem2  10050  ssfin4  10208  dffin7-2  10296  fin1a2lem11  10308  fin1a2lem12  10309  cfpwsdom  10482  elgch  10520  fpwwe2lem12  10540  canthp1lem2  10551  gch2  10573  elnn0  12390  un0addcl  12421  un0mulcl  12422  elxnn0  12463  ltxr  13016  elxr  13017  xrsupexmnf  13206  xrinfmexpnf  13207  supxrun  13217  ixxun  13263  difreicc  13386  iccsplit  13387  fzsplit2  13451  elfzp1  13476  uzsplit  13498  elfzp12  13505  fzosplit  13594  fzouzsplit  13596  elfzonlteqm1  13643  elfzo0l  13658  fzosplitsni  13681  elfzr  13683  elfzlmr  13684  hashnn0pnf  14251  hashf1lem2  14365  hash2pwpr  14385  pr2pwpr  14388  ccatrn  14499  cats1un  14630  fsumsplit  15650  sumsplit  15677  fprodsplit  15875  rpnnen2lem12  16136  sumeven  16300  sumodd  16301  saddisjlem  16377  lcmfunsnlem1  16550  lcmfunsnlem2lem1  16551  lcmfunsnlem2lem2  16552  lcmfunsnlem2  16553  coprmprod  16574  coprmproddvdslem  16575  nnnn0modprm0  16720  prm23lt5  16728  vdwapun  16888  ramubcl  16932  basprssdmsets  17134  mreexmrid  17551  lubun  18423  chnccats1  18533  smndex1basss  18815  smndex1mgm  18817  smndex1mndlem  18819  smndex1n0mnd  18822  symgextf1  19335  gsumzsplit  19841  gsumzunsnd  19870  gsumunsnfd  19871  dprddisj2  19955  dmdprdsplit2lem  19961  dmdprdsplit2  19962  dprdsplit  19964  cnfldfun  21307  cnfldfunOLD  21320  mplcoe1  21973  mplcoe5  21976  evlslem4  22012  mdetunilem9  22536  maducoeval2  22556  madugsum  22559  clslp  23064  islpi  23065  restntr  23098  pnfnei  23136  mnfnei  23137  iunconn  23344  refun0  23431  xkoptsub  23570  ptunhmeo  23724  fbun  23756  filconn  23799  fixufil  23838  ufildr  23847  alexsubALTlem2  23964  alexsubALTlem3  23965  alexsubALTlem4  23966  tsmssplit  24068  xrtgioo  24723  reconnlem2  24744  iccpnfcnv  24870  iccpnfhmeo  24871  rrxcph  25320  rrxdstprj1  25337  mbfss  25575  mbfmax  25578  itg2splitlem  25677  itg2split  25678  iblss2  25735  itgsplit  25765  limcdif  25805  ellimc2  25806  limcmpt  25812  limcres  25815  limccnp  25820  limccnp2  25821  limcco  25822  rollelem  25921  dvivthlem1  25941  dvne0  25944  lhop  25949  degltlem1  26005  ply1rem  26099  fta1glem2  26102  plypf1  26145  plyaddlem1  26146  plymullem1  26147  plycj  26211  plycjOLD  26213  ofmulrt  26217  taylfval  26294  abelthlem2  26370  abelthlem3  26371  reasinsin  26834  scvxcvx  26924  ppinprm  27090  chtnprm  27092  dchrfi  27194  lgsdir2  27269  2lgslem3  27343  2lgsoddprmlem3  27353  nosepdmlem  27623  ssltun1  27750  ssltun2  27751  addsproplem2  27914  addsuniflem  27945  negsid  27984  mulsproplem9  28064  ssltmul1  28087  ssltmul2  28088  precsexlem9  28154  precsexlem11  28156  sltonold  28199  usgrexmplef  29239  cffldtocusgr  29427  cffldtocusgrOLD  29428  vtxdun  29462  eucrct2eupth  30227  shunssi  31350  atomli  32364  atoml2i  32365  rmoun  32475  rmounid  32476  nelun  32495  suppovss  32666  isoun  32687  fzsplit3  32780  eliccioo  32918  gsumwun  33052  cycpmco2  33109  cyc3co2  33116  cycpmrn  33119  elrgspnlem2  33217  ply1dg3rt0irred  33553  lindsun  33659  lbsdiflsp0  33660  ordtconnlem1  33958  xrge0iifcnv  33967  xrge0iifiso  33969  xrge0iifhom  33971  esumsplit  34087  esumpad2  34090  measvuni  34248  sxbrsigalem0  34305  bnj1138  34821  bnj1137  35028  subfacp1lem4  35248  subfacp1lem5  35249  kur14lem7  35277  satfvsucsuc  35430  satfrnmapom  35435  satf0op  35442  satf0n0  35443  sat1el2xp  35444  fmlafvel  35450  isfmlasuc  35453  fmlaomn0  35455  satfv1fvfmla1  35488  2goelgoanfmla1  35489  mrsubcv  35575  mclsax  35634  brcup  36002  refssfne  36423  bj-eltag  37042  bj-0eltag  37043  bj-sngltag  37048  bj-projun  37059  bj-axbun  37101  bj-axadj  37106  bj-imdirco  37255  tan2h  37672  poimirlem2  37682  poimirlem8  37688  poimirlem18  37698  poimirlem21  37701  poimirlem22  37702  poimirlem23  37703  poimirlem24  37704  poimirlem25  37705  poimirlem27  37707  poimirlem29  37709  poimirlem31  37711  poimirlem32  37712  ftc1anclem1  37753  ftc1anclem5  37757  dvasin  37764  dvacos  37765  smprngopr  38112  dfsucmap3  38496  elpadd  39918  paddval0  39929  hdmaplem4  41893  mapdh9a  41908  unitscyglem2  42309  ofun  42354  lzunuz  42885  jm2.23  43113  unxpwdom3  43212  hbtlem5  43245  fzunt  43572  fzuntd  43573  fzunt1d  43574  fzuntgd  43575  rp-fakeinunass  43632  sqrtcvallem1  43748  frege133d  43882  frege83  44063  frege131  44111  frege133  44113  uneqsn  44142  clsk1indlem3  44160  ntrneixb  44212  ntrneix3  44214  ntrneix13  44216  radcnvrat  44431  bccbc  44462  undif3VD  44998  iunconnlem2  45051  permaxinf2lem  45129  fnchoice  45150  limciccioolb  45745  limcicciooub  45759  icccncfext  46009  cncfiooicclem1  46015  fourierdlem70  46298  fourierdlem80  46308  fourierdlem93  46321  fourierdlem101  46329  sge0split  46531  el1fzopredsuc  47449  iccpartltu  47549  iccpartgtl  47550  iccpartgt  47551  iccpartleu  47552  iccpartgel  47553  fmtno4prmfac  47696  31prm  47721  sbgoldbo  47911  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  wtgoldbnnsum4prm  47926  bgoldbnnsum3prm  47928  bgoldbtbndlem3  47931  bgoldbtbnd  47933  elclnbgrelnbgr  47949  clnbgrel  47952  clnbupgrel  47958  dfclnbgr6  47980  isubgr3stgrlem4  48093  usgrexmpl1tri  48149  usgrexmpl2nb0  48155  usgrexmpl2nb1  48156  usgrexmpl2nb2  48157  usgrexmpl2nb3  48158  usgrexmpl2nb4  48159  usgrexmpl2nb5  48160  usgrexmpl2trifr  48161  gpgprismgr4cycllem3  48221  gpgprismgr4cycllem7  48225  gpgprismgr4cycllem10  48228