Theorem elun 4110

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 3479	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3479	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3479	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 871	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2854	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2854	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 932	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3913	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3642	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   = wceq 1570   ∈ wcel 2146  Vcvv 3458   ∪ cun 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913

This theorem is used by:  elunnel1  4111  elunnel2  4112  uneqri  4113  uncom  4115  uneq1  4118  nfun  4127  unass  4128  ssun1  4134  elunant  4140  unss1  4141  ssequn1  4142  rexun  4152  elsymdif  4214  indi  4240  undi  4241  unineq  4244  undif3  4256  rabun2  4280  reuun2  4281  undif4  4430  ssundif  4453  dfpr2  4615  elunsn  4654  elpwunsn  4655  eltpg  4657  el7g  4661  pwpr  4871  pwtp  4872  uniun  4900  iinun2  5042  iunun  5064  iunxun  5065  iinuni  5069  brun  5167  trun  5234  pwssun  5558  opthprc  5730  xpundi  5735  xpundir  5736  difxp  6166  sossfld  6189  imadifssran  6207  imadifssranOLD  6208  elsuci  6437  elsucg  6438  elsuc2g  6439  funun  6589  mptun  6688  unima  6963  eqfnun  7039  unpreima  7065  ordsucun  7830  resf1extb  7940  fnse  8138  xpord2pred  8150  xpord3pred  8157  suppofssd  8208  reldmtpos  8239  dftpos4  8250  tpostpos  8251  frrlem12  8303  frrlem13  8304  oarec  8556  brdom2  8988  unfi  9165  unxpdomlem3  9228  domunfican  9291  dfsup2  9414  wemapso2lem  9524  unwdomg  9556  unxpwdom2  9560  cantnfp1lem3  9659  rankunb  9832  djur  9924  djuunxp  9926  eldju2ndl  9929  eldju2ndr  9930  djuun  9931  iscard3  10096  kmlem2  10154  ssfin4  10312  dffin7-2  10400  fin1a2lem11  10412  fin1a2lem12  10413  cfpwsdom  10587  elgch  10625  fpwwe2lem12  10645  canthp1lem2  10656  gch2  10678  elnn0  12524  un0addcl  12555  un0mulcl  12556  elxnn0  12597  ltxr  13158  elxr  13159  xrsupexmnf  13349  xrinfmexpnf  13350  supxrun  13360  ixxun  13406  difreicc  13529  iccsplit  13530  fzsplit2  13596  elfzp1  13621  uzsplit  13643  elfzp12  13650  fzosplit  13740  fzouzsplit  13742  elfzonlteqm1  13789  elfzo0l  13804  fzosplitsni  13827  elfzr  13829  elfzlmr  13830  hashnn0pnf  14398  hashf1lem2  14513  hash2pwpr  14533  pr2pwpr  14536  ccatrn  14647  cats1un  14782  fsumsplit  15818  sumsplit  15845  fprodsplit  16046  rpnnen2lem12  16306  sumeven  16470  sumodd  16471  saddisjlem  16547  lcmfunsnlem1  16720  lcmfunsnlem2lem1  16721  lcmfunsnlem2lem2  16722  lcmfunsnlem2  16723  coprmprod  16744  coprmproddvdslem  16745  nnnn0modprm0  16891  prm23lt5  16899  vdwapun  17059  ramubcl  17103  basprssdmsets  17306  mreexmrid  17724  lubun  18596  chnccats1  18706  smndex1basss  18998  smndex1mgm  19000  smndex1mndlem  19002  smndex1n0mnd  19005  symgextf1  19522  gsumzsplit  20028  gsumzunsnd  20057  gsumunsnfd  20058  dprddisj2  20142  dmdprdsplit2lem  20148  dmdprdsplit2  20149  dprdsplit  20151  cnfldfun  21573  mplcoe1  22225  mplcoe5  22228  evlslem4  22264  mdetunilem9  22814  maducoeval2  22834  madugsum  22837  clslp  23342  islpi  23343  restntr  23376  pnfnei  23414  mnfnei  23415  iunconn  23622  refun0  23709  xkoptsub  23848  ptunhmeo  24002  fbun  24034  filconn  24077  fixufil  24116  ufildr  24125  alexsubALTlem2  24242  alexsubALTlem3  24243  alexsubALTlem4  24244  tsmssplit  24346  xrtgioo  25001  reconnlem2  25022  iccpnfcnv  25140  iccpnfhmeo  25141  rrxcph  25588  rrxdstprj1  25605  mbfss  25842  mbfmax  25845  itg2splitlem  25944  itg2split  25945  iblss2  26002  itgsplit  26032  limcdif  26072  ellimc2  26073  limcmpt  26079  limcres  26082  limccnp  26087  limccnp2  26088  limcco  26089  rollelem  26185  dvivthlem1  26204  dvne0  26207  lhop  26212  degltlem1  26266  ply1rem  26360  fta1glem2  26363  plypf1  26406  plyaddlem1  26407  plymullem1  26408  plycj  26471  plycjOLD  26473  ofmulrt  26477  taylfval  26559  abelthlem2  26632  abelthlem3  26633  reasinsin  27098  scvxcvx  27187  ppinprm  27353  chtnprm  27355  dchrfi  27456  lgsdir2  27531  2lgslem3  27605  2lgsoddprmlem3  27615  nosepdmlem  27884  sltsun1  28018  sltsun2  28019  addsproplem2  28200  addsuniflem  28231  negsid  28271  mulsproplem9  28354  sltmuls1  28377  sltmuls2  28378  precsexlem9  28445  precsexlem11  28447  ltonold  28491  usgrexmplef  29646  cffldtocusgr  29834  vtxdun  29868  eucrct2eupth  30633  shunssi  31757  atomli  32771  atoml2i  32772  rmoun  32877  rmounid  32878  nelun  32896  suppovss  33063  isoun  33084  fzsplit3  33175  eliccioo  33287  gsumwun  33427  cycpmco2  33484  cyc3co2  33491  cycpmrn  33494  elrgspnlem2  33594  ply1dg3rt0irred  33905  lindsun  34046  lbsdiflsp0  34047  ordtconnlem1  34345  xrge0iifcnv  34354  xrge0iifiso  34356  xrge0iifhom  34358  esumsplit  34474  esumpad2  34477  measvuni  34635  sxbrsigalem0  34692  bnj1138  35208  bnj1137  35414  subfacp1lem4  35695  subfacp1lem5  35696  kur14lem7  35724  satfvsucsuc  35877  satfrnmapom  35882  satf0op  35889  satf0n0  35890  sat1el2xp  35891  fmlafvel  35897  isfmlasuc  35900  fmlaomn0  35902  satfv1fvfmla1  35935  2goelgoanfmla1  35936  mrsubcv  36022  mclsax  36081  brcup  36449  refssfne  36909  ttciunun  37062  bj-eltag  37653  bj-0eltag  37654  bj-sngltag  37659  bj-projun  37670  bj-axbun  37712  bj-axadj  37717  bj-imdirco  37874  tan2h  38303  poimirlem2  38313  poimirlem8  38319  poimirlem18  38329  poimirlem21  38332  poimirlem22  38333  poimirlem23  38334  poimirlem24  38335  poimirlem25  38336  poimirlem27  38338  poimirlem29  38340  poimirlem31  38342  poimirlem32  38343  ftc1anclem1  38384  ftc1anclem5  38388  dvasin  38395  dvacos  38396  smprngopr  38743  dfsucmap3  39152  elpadd  40613  paddval0  40624  hdmaplem4  42588  mapdh9a  42603  unitscyglem2  43003  ofun  43046  lzunuz  43539  jm2.23  43763  unxpwdom3  43862  hbtlem5  43895  fzunt  44221  fzuntd  44222  fzunt1d  44223  fzuntgd  44224  rp-fakeinunass  44281  sqrtcvallem1  44397  frege133d  44531  frege83  44712  frege131  44760  frege133  44762  uneqsn  44791  clsk1indlem3  44809  ntrneixb  44861  ntrneix3  44863  ntrneix13  44865  radcnvrat  45064  bccbc  45095  undif3VD  45630  iunconnlem2  45683  permaxinf2lem  45761  fnchoice  45789  limciccioolb  46377  limcicciooub  46391  icccncfext  46641  cncfiooicclem1  46647  fourierdlem70  46930  fourierdlem80  46940  fourierdlem93  46953  fourierdlem101  46961  sge0split  47163  el1fzopredsuc  48103  iccpartltu  48214  iccpartgtl  48215  iccpartgt  48216  iccpartleu  48217  iccpartgel  48218  fmtno4prmfac  48364  31prm  48389  sbgoldbo  48592  nnsum4primeseven  48605  nnsum4primesevenALTV  48606  wtgoldbnnsum4prm  48607  bgoldbnnsum3prm  48609  bgoldbtbndlem3  48612  bgoldbtbnd  48614  elclnbgrelnbgr  48630  clnbgrel  48633  clnbupgrel  48639  dfclnbgr6  48661  isubgr3stgrlem4  48774  usgrexmpl1tri  48830  usgrexmpl2nb0  48836  usgrexmpl2nb1  48837  usgrexmpl2nb2  48838  usgrexmpl2nb3  48839  usgrexmpl2nb4  48840  usgrexmpl2nb5  48841  usgrexmpl2trifr  48842  gpgprismgr4cycllem3  48902  gpgprismgr4cycllem7  48906  gpgprismgr4cycllem10  48909  smprngprmrng  49144