Theorem elun 4109

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

Syntax hints:   ↔ wb 209   ∨ wo 860   = wceq 1563   ∈ wcel 2145  Vcvv 3457   ∪ cun 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912

This theorem is referenced by:  elunnel1  4110  elunnel2  4111  uneqri  4112  uncom  4114  uneq1  4117  nfun  4126  unass  4127  ssun1  4133  elunant  4139  unss1  4140  ssequn1  4141  rexun  4151  elsymdif  4213  indi  4239  undi  4240  unineq  4243  undif3  4255  rabun2  4279  reuun2  4280  undif4  4424  ssundif  4444  dfpr2  4606  elunsn  4645  elpwunsn  4646  eltpg  4648  el7g  4652  pwpr  4862  pwtp  4863  uniun  4891  iinun2  5033  iunun  5055  iunxun  5056  iinuni  5060  brun  5156  trun  5223  pwssun  5544  opthprc  5716  xpundi  5721  xpundir  5722  imadifssran  6140  difxp  6153  sossfld  6176  elsuci  6419  elsucg  6420  elsuc2g  6421  funun  6571  mptun  6671  unima  6946  eqfnun  7022  unpreima  7048  ordsucun  7809  resf1extb  7919  fnse  8117  xpord2pred  8129  xpord3pred  8136  suppofssd  8187  reldmtpos  8218  dftpos4  8229  tpostpos  8230  frrlem12  8282  frrlem13  8283  oarec  8535  brdom2  8967  unfi  9143  unxpdomlem3  9206  domunfican  9269  dfsup2  9392  wemapso2lem  9502  unwdomg  9534  unxpwdom2  9538  cantnfp1lem3  9637  rankunb  9810  djur  9893  djuunxp  9895  eldju2ndl  9898  eldju2ndr  9899  djuun  9900  iscard3  10065  kmlem2  10123  ssfin4  10282  dffin7-2  10370  fin1a2lem11  10382  fin1a2lem12  10383  cfpwsdom  10557  elgch  10595  fpwwe2lem12  10615  canthp1lem2  10626  gch2  10648  elnn0  12497  un0addcl  12528  un0mulcl  12529  elxnn0  12570  ltxr  13131  elxr  13132  xrsupexmnf  13322  xrinfmexpnf  13323  supxrun  13333  ixxun  13379  difreicc  13502  iccsplit  13503  fzsplit2  13568  elfzp1  13593  uzsplit  13615  elfzp12  13622  fzosplit  13712  fzouzsplit  13714  elfzonlteqm1  13761  elfzo0l  13776  fzosplitsni  13799  elfzr  13801  elfzlmr  13802  hashnn0pnf  14369  hashf1lem2  14483  hash2pwpr  14503  pr2pwpr  14506  ccatrn  14617  cats1un  14748  fsumsplit  15782  sumsplit  15809  fprodsplit  16010  rpnnen2lem12  16271  sumeven  16435  sumodd  16436  saddisjlem  16512  lcmfunsnlem1  16685  lcmfunsnlem2lem1  16686  lcmfunsnlem2lem2  16687  lcmfunsnlem2  16688  coprmprod  16709  coprmproddvdslem  16710  nnnn0modprm0  16856  prm23lt5  16864  vdwapun  17024  ramubcl  17068  basprssdmsets  17271  mreexmrid  17689  lubun  18561  chnccats1  18671  smndex1basss  18957  smndex1mgm  18959  smndex1mndlem  18961  smndex1n0mnd  18964  symgextf1  19482  gsumzsplit  19988  gsumzunsnd  20017  gsumunsnfd  20018  dprddisj2  20102  dmdprdsplit2lem  20108  dmdprdsplit2  20109  dprdsplit  20111  cnfldfun  21496  mplcoe1  22148  mplcoe5  22151  evlslem4  22187  mdetunilem9  22738  maducoeval2  22758  madugsum  22761  clslp  23266  islpi  23267  restntr  23300  pnfnei  23338  mnfnei  23339  iunconn  23546  refun0  23633  xkoptsub  23772  ptunhmeo  23926  fbun  23958  filconn  24001  fixufil  24040  ufildr  24049  alexsubALTlem2  24166  alexsubALTlem3  24167  alexsubALTlem4  24168  tsmssplit  24270  xrtgioo  24925  reconnlem2  24946  iccpnfcnv  25064  iccpnfhmeo  25065  rrxcph  25512  rrxdstprj1  25529  mbfss  25766  mbfmax  25769  itg2splitlem  25868  itg2split  25869  iblss2  25926  itgsplit  25956  limcdif  25996  ellimc2  25997  limcmpt  26003  limcres  26006  limccnp  26011  limccnp2  26012  limcco  26013  rollelem  26109  dvivthlem1  26128  dvne0  26131  lhop  26136  degltlem1  26190  ply1rem  26284  fta1glem2  26287  plypf1  26330  plyaddlem1  26331  plymullem1  26332  plycj  26395  plycjOLD  26397  ofmulrt  26401  taylfval  26480  abelthlem2  26553  abelthlem3  26554  reasinsin  27019  scvxcvx  27108  ppinprm  27274  chtnprm  27276  dchrfi  27377  lgsdir2  27452  2lgslem3  27526  2lgsoddprmlem3  27536  nosepdmlem  27805  sltsun1  27939  sltsun2  27940  addsproplem2  28121  addsuniflem  28152  negsid  28192  mulsproplem9  28275  sltmuls1  28298  sltmuls2  28299  precsexlem9  28366  precsexlem11  28368  ltonold  28412  usgrexmplef  29518  cffldtocusgr  29706  vtxdun  29740  eucrct2eupth  30505  shunssi  31629  atomli  32643  atoml2i  32644  rmoun  32750  rmounid  32751  nelun  32769  suppovss  32938  isoun  32959  fzsplit3  33050  eliccioo  33163  gsumwun  33309  cycpmco2  33366  cyc3co2  33373  cycpmrn  33376  elrgspnlem2  33476  ply1dg3rt0irred  33791  lindsun  33932  lbsdiflsp0  33933  ordtconnlem1  34231  xrge0iifcnv  34240  xrge0iifiso  34242  xrge0iifhom  34244  esumsplit  34360  esumpad2  34363  measvuni  34521  sxbrsigalem0  34578  bnj1138  35094  bnj1137  35300  subfacp1lem4  35546  subfacp1lem5  35547  kur14lem7  35575  satfvsucsuc  35728  satfrnmapom  35733  satf0op  35740  satf0n0  35741  sat1el2xp  35742  fmlafvel  35748  isfmlasuc  35751  fmlaomn0  35753  satfv1fvfmla1  35786  2goelgoanfmla1  35787  mrsubcv  35873  mclsax  35932  brcup  36300  refssfne  36731  ttciunun  36884  bj-eltag  37474  bj-0eltag  37475  bj-sngltag  37480  bj-projun  37491  bj-axbun  37533  bj-axadj  37538  bj-imdirco  37694  tan2h  38123  poimirlem2  38133  poimirlem8  38139  poimirlem18  38149  poimirlem21  38152  poimirlem22  38153  poimirlem23  38154  poimirlem24  38155  poimirlem25  38156  poimirlem27  38158  poimirlem29  38160  poimirlem31  38162  poimirlem32  38163  ftc1anclem1  38204  ftc1anclem5  38208  dvasin  38215  dvacos  38216  smprngopr  38563  dfsucmap3  38974  elpadd  40435  paddval0  40446  hdmaplem4  42410  mapdh9a  42425  unitscyglem2  42825  ofun  42866  lzunuz  43361  jm2.23  43585  unxpwdom3  43684  hbtlem5  43717  fzunt  44043  fzuntd  44044  fzunt1d  44045  fzuntgd  44046  rp-fakeinunass  44103  sqrtcvallem1  44219  frege133d  44353  frege83  44534  frege131  44582  frege133  44584  uneqsn  44613  clsk1indlem3  44631  ntrneixb  44683  ntrneix3  44685  ntrneix13  44687  radcnvrat  44888  bccbc  44919  undif3VD  45455  iunconnlem2  45508  permaxinf2lem  45586  fnchoice  45607  limciccioolb  46195  limcicciooub  46209  icccncfext  46459  cncfiooicclem1  46465  fourierdlem70  46748  fourierdlem80  46758  fourierdlem93  46771  fourierdlem101  46779  sge0split  46981  el1fzopredsuc  47918  iccpartltu  48029  iccpartgtl  48030  iccpartgt  48031  iccpartleu  48032  iccpartgel  48033  fmtno4prmfac  48179  31prm  48204  sbgoldbo  48407  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  wtgoldbnnsum4prm  48422  bgoldbnnsum3prm  48424  bgoldbtbndlem3  48427  bgoldbtbnd  48429  elclnbgrelnbgr  48445  clnbgrel  48448  clnbupgrel  48454  dfclnbgr6  48476  isubgr3stgrlem4  48589  usgrexmpl1tri  48645  usgrexmpl2nb0  48651  usgrexmpl2nb1  48652  usgrexmpl2nb2  48653  usgrexmpl2nb3  48654  usgrexmpl2nb4  48655  usgrexmpl2nb5  48656  usgrexmpl2trifr  48657  gpgprismgr4cycllem3  48717  gpgprismgr4cycllem7  48721  gpgprismgr4cycllem10  48724  smprngprmrng  48959