Theorem elun 4108

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

Syntax hints:   ↔ wb 209   ∨ wo 860   = wceq 1570   ∈ wcel 2143  Vcvv 3455   ∪ cun 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911

This theorem is referenced by:  elunnel1  4109  elunnel2  4110  uneqri  4111  uncom  4113  uneq1  4116  nfun  4125  unass  4126  ssun1  4132  elunant  4138  unss1  4139  ssequn1  4140  rexun  4150  elsymdif  4212  indi  4238  undi  4239  unineq  4242  undif3  4254  rabun2  4278  reuun2  4279  undif4  4428  ssundif  4449  dfpr2  4611  elunsn  4650  elpwunsn  4651  eltpg  4653  el7g  4657  pwpr  4867  pwtp  4868  uniun  4896  iinun2  5038  iunun  5060  iunxun  5061  iinuni  5065  brun  5163  trun  5230  pwssun  5555  opthprc  5727  xpundi  5732  xpundir  5733  difxp  6163  sossfld  6186  imadifssran  6204  imadifssranOLD  6205  elsuci  6432  elsucg  6433  elsuc2g  6434  funun  6584  mptun  6683  unima  6958  eqfnun  7034  unpreima  7060  ordsucun  7822  resf1extb  7932  fnse  8130  xpord2pred  8142  xpord3pred  8149  suppofssd  8200  reldmtpos  8231  dftpos4  8242  tpostpos  8243  frrlem12  8295  frrlem13  8296  oarec  8548  brdom2  8980  unfi  9156  unxpdomlem3  9219  domunfican  9282  dfsup2  9405  wemapso2lem  9515  unwdomg  9547  unxpwdom2  9551  cantnfp1lem3  9650  rankunb  9823  djur  9906  djuunxp  9908  eldju2ndl  9911  eldju2ndr  9912  djuun  9913  iscard3  10078  kmlem2  10136  ssfin4  10295  dffin7-2  10383  fin1a2lem11  10395  fin1a2lem12  10396  cfpwsdom  10570  elgch  10608  fpwwe2lem12  10628  canthp1lem2  10639  gch2  10661  elnn0  12507  un0addcl  12538  un0mulcl  12539  elxnn0  12580  ltxr  13141  elxr  13142  xrsupexmnf  13332  xrinfmexpnf  13333  supxrun  13343  ixxun  13389  difreicc  13512  iccsplit  13513  fzsplit2  13579  elfzp1  13604  uzsplit  13626  elfzp12  13633  fzosplit  13723  fzouzsplit  13725  elfzonlteqm1  13772  elfzo0l  13787  fzosplitsni  13810  elfzr  13812  elfzlmr  13813  hashnn0pnf  14380  hashf1lem2  14495  hash2pwpr  14515  pr2pwpr  14518  ccatrn  14629  cats1un  14760  fsumsplit  15794  sumsplit  15821  fprodsplit  16022  rpnnen2lem12  16282  sumeven  16446  sumodd  16447  saddisjlem  16523  lcmfunsnlem1  16696  lcmfunsnlem2lem1  16697  lcmfunsnlem2lem2  16698  lcmfunsnlem2  16699  coprmprod  16720  coprmproddvdslem  16721  nnnn0modprm0  16867  prm23lt5  16875  vdwapun  17035  ramubcl  17079  basprssdmsets  17282  mreexmrid  17700  lubun  18572  chnccats1  18682  smndex1basss  18968  smndex1mgm  18970  smndex1mndlem  18972  smndex1n0mnd  18975  symgextf1  19492  gsumzsplit  19998  gsumzunsnd  20027  gsumunsnfd  20028  dprddisj2  20112  dmdprdsplit2lem  20118  dmdprdsplit2  20119  dprdsplit  20121  cnfldfun  21517  mplcoe1  22169  mplcoe5  22172  evlslem4  22208  mdetunilem9  22758  maducoeval2  22778  madugsum  22781  clslp  23286  islpi  23287  restntr  23320  pnfnei  23358  mnfnei  23359  iunconn  23566  refun0  23653  xkoptsub  23792  ptunhmeo  23946  fbun  23978  filconn  24021  fixufil  24060  ufildr  24069  alexsubALTlem2  24186  alexsubALTlem3  24187  alexsubALTlem4  24188  tsmssplit  24290  xrtgioo  24945  reconnlem2  24966  iccpnfcnv  25084  iccpnfhmeo  25085  rrxcph  25532  rrxdstprj1  25549  mbfss  25786  mbfmax  25789  itg2splitlem  25888  itg2split  25889  iblss2  25946  itgsplit  25976  limcdif  26016  ellimc2  26017  limcmpt  26023  limcres  26026  limccnp  26031  limccnp2  26032  limcco  26033  rollelem  26129  dvivthlem1  26148  dvne0  26151  lhop  26156  degltlem1  26210  ply1rem  26304  fta1glem2  26307  plypf1  26350  plyaddlem1  26351  plymullem1  26352  plycj  26415  plycjOLD  26417  ofmulrt  26421  taylfval  26500  abelthlem2  26573  abelthlem3  26574  reasinsin  27039  scvxcvx  27128  ppinprm  27294  chtnprm  27296  dchrfi  27397  lgsdir2  27472  2lgslem3  27546  2lgsoddprmlem3  27556  nosepdmlem  27825  sltsun1  27959  sltsun2  27960  addsproplem2  28141  addsuniflem  28172  negsid  28212  mulsproplem9  28295  sltmuls1  28318  sltmuls2  28319  precsexlem9  28386  precsexlem11  28388  ltonold  28432  usgrexmplef  29587  cffldtocusgr  29775  vtxdun  29809  eucrct2eupth  30574  shunssi  31698  atomli  32712  atoml2i  32713  rmoun  32818  rmounid  32819  nelun  32837  suppovss  33004  isoun  33025  fzsplit3  33116  eliccioo  33228  gsumwun  33374  cycpmco2  33431  cyc3co2  33438  cycpmrn  33441  elrgspnlem2  33541  ply1dg3rt0irred  33852  lindsun  33993  lbsdiflsp0  33994  ordtconnlem1  34292  xrge0iifcnv  34301  xrge0iifiso  34303  xrge0iifhom  34305  esumsplit  34421  esumpad2  34424  measvuni  34582  sxbrsigalem0  34639  bnj1138  35155  bnj1137  35361  subfacp1lem4  35653  subfacp1lem5  35654  kur14lem7  35682  satfvsucsuc  35835  satfrnmapom  35840  satf0op  35847  satf0n0  35848  sat1el2xp  35849  fmlafvel  35855  isfmlasuc  35858  fmlaomn0  35860  satfv1fvfmla1  35893  2goelgoanfmla1  35894  mrsubcv  35980  mclsax  36039  brcup  36407  refssfne  36847  ttciunun  37000  bj-eltag  37591  bj-0eltag  37592  bj-sngltag  37597  bj-projun  37608  bj-axbun  37650  bj-axadj  37655  bj-imdirco  37812  tan2h  38241  poimirlem2  38251  poimirlem8  38257  poimirlem18  38267  poimirlem21  38270  poimirlem22  38271  poimirlem23  38272  poimirlem24  38273  poimirlem25  38274  poimirlem27  38276  poimirlem29  38278  poimirlem31  38280  poimirlem32  38281  ftc1anclem1  38322  ftc1anclem5  38326  dvasin  38333  dvacos  38334  smprngopr  38681  dfsucmap3  39090  elpadd  40551  paddval0  40562  hdmaplem4  42526  mapdh9a  42541  unitscyglem2  42941  ofun  42984  lzunuz  43479  jm2.23  43703  unxpwdom3  43802  hbtlem5  43835  fzunt  44161  fzuntd  44162  fzunt1d  44163  fzuntgd  44164  rp-fakeinunass  44221  sqrtcvallem1  44337  frege133d  44471  frege83  44652  frege131  44700  frege133  44702  uneqsn  44731  clsk1indlem3  44749  ntrneixb  44801  ntrneix3  44803  ntrneix13  44805  radcnvrat  45004  bccbc  45035  undif3VD  45570  iunconnlem2  45623  permaxinf2lem  45701  fnchoice  45729  limciccioolb  46317  limcicciooub  46331  icccncfext  46581  cncfiooicclem1  46587  fourierdlem70  46870  fourierdlem80  46880  fourierdlem93  46893  fourierdlem101  46901  sge0split  47103  el1fzopredsuc  48040  iccpartltu  48151  iccpartgtl  48152  iccpartgt  48153  iccpartleu  48154  iccpartgel  48155  fmtno4prmfac  48301  31prm  48326  sbgoldbo  48529  nnsum4primeseven  48542  nnsum4primesevenALTV  48543  wtgoldbnnsum4prm  48544  bgoldbnnsum3prm  48546  bgoldbtbndlem3  48549  bgoldbtbnd  48551  elclnbgrelnbgr  48567  clnbgrel  48570  clnbupgrel  48576  dfclnbgr6  48598  isubgr3stgrlem4  48711  usgrexmpl1tri  48767  usgrexmpl2nb0  48773  usgrexmpl2nb1  48774  usgrexmpl2nb2  48775  usgrexmpl2nb3  48776  usgrexmpl2nb4  48777  usgrexmpl2nb5  48778  usgrexmpl2trifr  48779  gpgprismgr4cycllem3  48839  gpgprismgr4cycllem7  48843  gpgprismgr4cycllem10  48846  smprngprmrng  49081