Theorem elun 4079

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 3440	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3440	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3440	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 853	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2826	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2826	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 915	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3888	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3604	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 379	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 205   ∨ wo 843   = wceq 1539   ∈ wcel 2108  Vcvv 3422   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888

This theorem is referenced by:  elunnel1  4080  uneqri  4081  uncom  4083  uneq1  4086  unass  4096  ssun1  4102  elunant  4108  unss1  4109  ssequn1  4110  rexun  4120  elsymdif  4178  indi  4204  undi  4205  unineq  4208  undif3  4221  rabun2  4244  reuun2  4245  undif4  4397  ssundif  4415  dfpr2  4577  elpwunsn  4616  eltpg  4618  pwpr  4830  pwtp  4831  uniun  4861  iinun2  4998  iunun  5018  iunxun  5019  iinuni  5023  brun  5121  pwunssOLD  5475  pwssun  5476  opthprc  5642  xpundi  5646  xpundir  5647  difxp  6056  sossfld  6078  elsuci  6317  elsucg  6318  elsuc2g  6319  funun  6464  mptun  6563  unima  6825  unpreima  6922  suceloni  7635  ordsucun  7647  fnse  7945  suppofssd  7990  reldmtpos  8021  dftpos4  8032  tpostpos  8033  frrlem12  8084  frrlem13  8085  wfrlem14OLD  8124  wfrlem15OLD  8125  oarec  8355  brdom2  8725  unfi  8917  unxpdomlem3  8958  domunfican  9017  dfsup2  9133  wemapso2lem  9241  unwdomg  9273  unxpwdom2  9277  cantnfp1lem3  9368  dftrpred3g  9412  rankunb  9539  djur  9608  djuunxp  9610  eldju2ndl  9613  eldju2ndr  9614  djuun  9615  iscard3  9780  kmlem2  9838  ssfin4  9997  dffin7-2  10085  fin1a2lem11  10097  fin1a2lem12  10098  cfpwsdom  10271  elgch  10309  fpwwe2lem12  10329  canthp1lem2  10340  gch2  10362  elnn0  12165  un0addcl  12196  un0mulcl  12197  elxnn0  12237  ltxr  12780  elxr  12781  xrsupexmnf  12968  xrinfmexpnf  12969  supxrun  12979  ixxun  13024  difreicc  13145  iccsplit  13146  fzsplit2  13210  elfzp1  13235  uzsplit  13257  elfzp12  13264  fzosplit  13348  fzouzsplit  13350  elfzonlteqm1  13391  elfzo0l  13405  fzosplitsni  13426  elfzr  13428  elfzlmr  13429  hashnn0pnf  13984  hashf1lem2  14098  hash2pwpr  14118  pr2pwpr  14121  ccatrn  14222  cats1un  14362  fsumsplit  15381  sumsplit  15408  fprodsplit  15604  rpnnen2lem12  15862  sumeven  16024  sumodd  16025  saddisjlem  16099  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  lcmfunsnlem2  16273  coprmprod  16294  coprmproddvdslem  16295  nnnn0modprm0  16435  prm23lt5  16443  vdwapun  16603  ramubcl  16647  basprssdmsets  16853  mreexmrid  17269  lubun  18148  smndex1basss  18459  smndex1mgm  18461  smndex1mndlem  18463  smndex1n0mnd  18466  symgextf1  18944  gsumzsplit  19443  gsumzunsnd  19472  gsumunsnfd  19473  dprddisj2  19557  dmdprdsplit2lem  19563  dmdprdsplit2  19564  dprdsplit  19566  cnfldfunALT  20523  mplcoe1  21148  mplcoe5  21151  evlslem4  21194  mdetunilem9  21677  maducoeval2  21697  madugsum  21700  clslp  22207  islpi  22208  restntr  22241  pnfnei  22279  mnfnei  22280  iunconn  22487  refun0  22574  xkoptsub  22713  ptunhmeo  22867  fbun  22899  filconn  22942  fixufil  22981  ufildr  22990  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  tsmssplit  23211  xrtgioo  23875  reconnlem2  23896  iccpnfcnv  24013  iccpnfhmeo  24014  rrxcph  24461  rrxdstprj1  24478  mbfss  24715  mbfmax  24718  itg2splitlem  24818  itg2split  24819  iblss2  24875  itgsplit  24905  limcdif  24945  ellimc2  24946  limcmpt  24952  limcres  24955  limccnp  24960  limccnp2  24961  limcco  24962  rollelem  25058  dvivthlem1  25077  dvne0  25080  lhop  25085  degltlem1  25142  ply1rem  25233  fta1glem2  25236  plypf1  25278  plyaddlem1  25279  plymullem1  25280  plycj  25343  ofmulrt  25347  taylfval  25423  abelthlem2  25496  abelthlem3  25497  reasinsin  25951  scvxcvx  26040  ppinprm  26206  chtnprm  26208  dchrfi  26308  lgsdir2  26383  2lgslem3  26457  2lgsoddprmlem3  26467  usgrexmplef  27529  cffldtocusgr  27717  vtxdun  27751  eucrct2eupth  28510  shunssi  29631  atomli  30645  atoml2i  30646  rmoun  30743  rmounid  30744  elunsn  30759  nelun  30760  suppovss  30919  isoun  30936  fzsplit3  31017  eliccioo  31107  cycpmco2  31302  cyc3co2  31309  cycpmrn  31312  lindsun  31608  lbsdiflsp0  31609  ordtconnlem1  31776  xrge0iifcnv  31785  xrge0iifiso  31787  xrge0iifhom  31789  esumsplit  31921  esumpad2  31924  measvuni  32082  sxbrsigalem0  32138  bnj1138  32668  bnj1137  32875  subfacp1lem4  33045  subfacp1lem5  33046  kur14lem7  33074  satfvsucsuc  33227  satfrnmapom  33232  satf0op  33239  satf0n0  33240  sat1el2xp  33241  fmlafvel  33247  isfmlasuc  33250  fmlaomn0  33252  satfv1fvfmla1  33285  2goelgoanfmla1  33286  mrsubcv  33372  mclsax  33431  xpord2pred  33719  xpord3pred  33725  nosepdmlem  33813  ssltun1  33929  ssltun2  33930  brcup  34168  refssfne  34474  bj-eltag  35094  bj-0eltag  35095  bj-sngltag  35100  bj-projun  35111  bj-imdirco  35288  tan2h  35696  poimirlem2  35706  poimirlem8  35712  poimirlem18  35722  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem27  35731  poimirlem29  35733  poimirlem31  35735  poimirlem32  35736  ftc1anclem1  35777  ftc1anclem5  35781  dvasin  35788  dvacos  35789  eqfnun  35807  smprngopr  36137  elpadd  37740  paddval0  37751  hdmaplem4  39715  mapdh9a  39730  ofun  40137  lzunuz  40506  jm2.23  40734  unxpwdom3  40836  hbtlem5  40869  rp-fakeinunass  41020  sqrtcvallem1  41128  frege133d  41262  frege83  41443  frege131  41491  frege133  41493  uneqsn  41522  clsk1indlem3  41542  ntrneixb  41594  ntrneix3  41596  ntrneix13  41598  radcnvrat  41821  bccbc  41852  undif3VD  42391  iunconnlem2  42444  fnchoice  42461  elunnel2  42471  limciccioolb  43052  limcicciooub  43068  icccncfext  43318  cncfiooicclem1  43324  fourierdlem70  43607  fourierdlem80  43617  fourierdlem93  43630  fourierdlem101  43638  sge0split  43837  el1fzopredsuc  44705  iccpartltu  44765  iccpartgtl  44766  iccpartgt  44767  iccpartleu  44768  iccpartgel  44769  fmtno4prmfac  44912  31prm  44937  sbgoldbo  45127  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  bgoldbtbndlem3  45147  bgoldbtbnd  45149