Theorem elun 4094

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 3451	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3451	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3451	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 858	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2825	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2825	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 919	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3895	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3624	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 206   ∨ wo 848   = wceq 1542   ∈ wcel 2114  Vcvv 3430   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895

This theorem is referenced by:  elunnel1  4095  elunnel2  4096  uneqri  4097  uncom  4099  uneq1  4102  nfun  4111  unass  4113  ssun1  4119  elunant  4125  unss1  4126  ssequn1  4127  rexun  4137  elsymdif  4199  indi  4225  undi  4226  unineq  4229  undif3  4241  rabun2  4265  reuun2  4266  undif4  4408  ssundif  4428  dfpr2  4589  elunsn  4628  elpwunsn  4629  eltpg  4631  el7g  4635  pwpr  4845  pwtp  4846  uniun  4874  iinun2  5016  iunun  5036  iunxun  5037  iinuni  5041  brun  5137  pwssun  5516  opthprc  5688  xpundi  5693  xpundir  5694  imadifssran  6109  difxp  6122  sossfld  6144  elsuci  6386  elsucg  6387  elsuc2g  6388  funun  6538  mptun  6638  unima  6909  eqfnun  6983  unpreima  7009  ordsucun  7769  resf1extb  7878  fnse  8076  xpord2pred  8088  xpord3pred  8095  suppofssd  8146  reldmtpos  8177  dftpos4  8188  tpostpos  8189  frrlem12  8240  frrlem13  8241  oarec  8490  brdom2  8922  unfi  9098  unxpdomlem3  9161  domunfican  9225  dfsup2  9350  wemapso2lem  9460  unwdomg  9492  unxpwdom2  9496  cantnfp1lem3  9592  rankunb  9765  djur  9834  djuunxp  9836  eldju2ndl  9839  eldju2ndr  9840  djuun  9841  iscard3  10006  kmlem2  10065  ssfin4  10223  dffin7-2  10311  fin1a2lem11  10323  fin1a2lem12  10324  cfpwsdom  10498  elgch  10536  fpwwe2lem12  10556  canthp1lem2  10567  gch2  10589  elnn0  12430  un0addcl  12461  un0mulcl  12462  elxnn0  12503  ltxr  13057  elxr  13058  xrsupexmnf  13248  xrinfmexpnf  13249  supxrun  13259  ixxun  13305  difreicc  13428  iccsplit  13429  fzsplit2  13494  elfzp1  13519  uzsplit  13541  elfzp12  13548  fzosplit  13638  fzouzsplit  13640  elfzonlteqm1  13687  elfzo0l  13702  fzosplitsni  13725  elfzr  13727  elfzlmr  13728  hashnn0pnf  14295  hashf1lem2  14409  hash2pwpr  14429  pr2pwpr  14432  ccatrn  14543  cats1un  14674  fsumsplit  15694  sumsplit  15721  fprodsplit  15922  rpnnen2lem12  16183  sumeven  16347  sumodd  16348  saddisjlem  16424  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfunsnlem2  16600  coprmprod  16621  coprmproddvdslem  16622  nnnn0modprm0  16768  prm23lt5  16776  vdwapun  16936  ramubcl  16980  basprssdmsets  17182  mreexmrid  17600  lubun  18472  chnccats1  18582  smndex1basss  18867  smndex1mgm  18869  smndex1mndlem  18871  smndex1n0mnd  18874  symgextf1  19387  gsumzsplit  19893  gsumzunsnd  19922  gsumunsnfd  19923  dprddisj2  20007  dmdprdsplit2lem  20013  dmdprdsplit2  20014  dprdsplit  20016  cnfldfun  21358  cnfldfunOLD  21371  mplcoe1  22025  mplcoe5  22028  evlslem4  22064  mdetunilem9  22595  maducoeval2  22615  madugsum  22618  clslp  23123  islpi  23124  restntr  23157  pnfnei  23195  mnfnei  23196  iunconn  23403  refun0  23490  xkoptsub  23629  ptunhmeo  23783  fbun  23815  filconn  23858  fixufil  23897  ufildr  23906  alexsubALTlem2  24023  alexsubALTlem3  24024  alexsubALTlem4  24025  tsmssplit  24127  xrtgioo  24782  reconnlem2  24803  iccpnfcnv  24921  iccpnfhmeo  24922  rrxcph  25369  rrxdstprj1  25386  mbfss  25623  mbfmax  25626  itg2splitlem  25725  itg2split  25726  iblss2  25783  itgsplit  25813  limcdif  25853  ellimc2  25854  limcmpt  25860  limcres  25863  limccnp  25868  limccnp2  25869  limcco  25870  rollelem  25966  dvivthlem1  25985  dvne0  25988  lhop  25993  degltlem1  26047  ply1rem  26141  fta1glem2  26144  plypf1  26187  plyaddlem1  26188  plymullem1  26189  plycj  26252  plycjOLD  26254  ofmulrt  26258  taylfval  26335  abelthlem2  26410  abelthlem3  26411  reasinsin  26873  scvxcvx  26963  ppinprm  27129  chtnprm  27131  dchrfi  27232  lgsdir2  27307  2lgslem3  27381  2lgsoddprmlem3  27391  nosepdmlem  27661  sltsun1  27794  sltsun2  27795  addsproplem2  27976  addsuniflem  28007  negsid  28047  mulsproplem9  28130  sltmuls1  28153  sltmuls2  28154  precsexlem9  28221  precsexlem11  28223  ltonold  28267  usgrexmplef  29342  cffldtocusgr  29530  cffldtocusgrOLD  29531  vtxdun  29565  eucrct2eupth  30330  shunssi  31454  atomli  32468  atoml2i  32469  rmoun  32578  rmounid  32579  nelun  32598  suppovss  32769  isoun  32790  fzsplit3  32881  eliccioo  33005  gsumwun  33152  cycpmco2  33209  cyc3co2  33216  cycpmrn  33219  elrgspnlem2  33319  ply1dg3rt0irred  33659  lindsun  33785  lbsdiflsp0  33786  ordtconnlem1  34084  xrge0iifcnv  34093  xrge0iifiso  34095  xrge0iifhom  34097  esumsplit  34213  esumpad2  34216  measvuni  34374  sxbrsigalem0  34431  bnj1138  34947  bnj1137  35153  subfacp1lem4  35381  subfacp1lem5  35382  kur14lem7  35410  satfvsucsuc  35563  satfrnmapom  35568  satf0op  35575  satf0n0  35576  sat1el2xp  35577  fmlafvel  35583  isfmlasuc  35586  fmlaomn0  35588  satfv1fvfmla1  35621  2goelgoanfmla1  35622  mrsubcv  35708  mclsax  35767  brcup  36135  refssfne  36556  ttciunun  36709  bj-eltag  37300  bj-0eltag  37301  bj-sngltag  37306  bj-projun  37317  bj-axbun  37359  bj-axadj  37364  bj-imdirco  37520  tan2h  37947  poimirlem2  37957  poimirlem8  37963  poimirlem18  37973  poimirlem21  37976  poimirlem22  37977  poimirlem23  37978  poimirlem24  37979  poimirlem25  37980  poimirlem27  37982  poimirlem29  37984  poimirlem31  37986  poimirlem32  37987  ftc1anclem1  38028  ftc1anclem5  38032  dvasin  38039  dvacos  38040  smprngopr  38387  dfsucmap3  38798  elpadd  40259  paddval0  40270  hdmaplem4  42234  mapdh9a  42249  unitscyglem2  42649  ofun  42691  lzunuz  43214  jm2.23  43442  unxpwdom3  43541  hbtlem5  43574  fzunt  43900  fzuntd  43901  fzunt1d  43902  fzuntgd  43903  rp-fakeinunass  43960  sqrtcvallem1  44076  frege133d  44210  frege83  44391  frege131  44439  frege133  44441  uneqsn  44470  clsk1indlem3  44488  ntrneixb  44540  ntrneix3  44542  ntrneix13  44544  radcnvrat  44759  bccbc  44790  undif3VD  45326  iunconnlem2  45379  permaxinf2lem  45457  fnchoice  45478  limciccioolb  46069  limcicciooub  46083  icccncfext  46333  cncfiooicclem1  46339  fourierdlem70  46622  fourierdlem80  46632  fourierdlem93  46645  fourierdlem101  46653  sge0split  46855  el1fzopredsuc  47786  iccpartltu  47897  iccpartgtl  47898  iccpartgt  47899  iccpartleu  47900  iccpartgel  47901  fmtno4prmfac  48047  31prm  48072  sbgoldbo  48275  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  wtgoldbnnsum4prm  48290  bgoldbnnsum3prm  48292  bgoldbtbndlem3  48295  bgoldbtbnd  48297  elclnbgrelnbgr  48313  clnbgrel  48316  clnbupgrel  48322  dfclnbgr6  48344  isubgr3stgrlem4  48457  usgrexmpl1tri  48513  usgrexmpl2nb0  48519  usgrexmpl2nb1  48520  usgrexmpl2nb2  48521  usgrexmpl2nb3  48522  usgrexmpl2nb4  48523  usgrexmpl2nb5  48524  usgrexmpl2trifr  48525  gpgprismgr4cycllem3  48585  gpgprismgr4cycllem7  48589  gpgprismgr4cycllem10  48592