Theorem elun 4106

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 3474	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3474	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3474	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 868	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2849	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2849	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 929	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3909	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3639	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 380	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 208   ∨ wo 858   = wceq 1559   ∈ wcel 2141  Vcvv 3453   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909

This theorem is referenced by:  elunnel1  4107  elunnel2  4108  uneqri  4109  uncom  4111  uneq1  4114  nfun  4123  unass  4124  ssun1  4130  elunant  4136  unss1  4137  ssequn1  4138  rexun  4148  elsymdif  4210  indi  4236  undi  4237  unineq  4240  undif3  4252  rabun2  4276  reuun2  4277  undif4  4420  ssundif  4440  dfpr2  4602  elunsn  4641  elpwunsn  4642  eltpg  4644  el7g  4648  pwpr  4858  pwtp  4859  uniun  4887  iinun2  5029  iunun  5049  iunxun  5050  iinuni  5054  brun  5150  trun  5217  pwssun  5537  opthprc  5709  xpundi  5714  xpundir  5715  imadifssran  6133  difxp  6146  sossfld  6168  elsuci  6411  elsucg  6412  elsuc2g  6413  funun  6563  mptun  6663  unima  6938  eqfnun  7014  unpreima  7040  ordsucun  7801  resf1extb  7911  fnse  8108  xpord2pred  8120  xpord3pred  8127  suppofssd  8178  reldmtpos  8209  dftpos4  8220  tpostpos  8221  frrlem12  8273  frrlem13  8274  oarec  8526  brdom2  8959  unfi  9135  unxpdomlem3  9198  domunfican  9262  dfsup2  9387  wemapso2lem  9497  unwdomg  9529  unxpwdom2  9533  cantnfp1lem3  9632  rankunb  9805  djur  9874  djuunxp  9876  eldju2ndl  9879  eldju2ndr  9880  djuun  9881  iscard3  10046  kmlem2  10105  ssfin4  10264  dffin7-2  10352  fin1a2lem11  10364  fin1a2lem12  10365  cfpwsdom  10539  elgch  10577  fpwwe2lem12  10597  canthp1lem2  10608  gch2  10630  elnn0  12480  un0addcl  12511  un0mulcl  12512  elxnn0  12553  ltxr  13114  elxr  13115  xrsupexmnf  13305  xrinfmexpnf  13306  supxrun  13316  ixxun  13362  difreicc  13485  iccsplit  13486  fzsplit2  13551  elfzp1  13576  uzsplit  13598  elfzp12  13605  fzosplit  13695  fzouzsplit  13697  elfzonlteqm1  13744  elfzo0l  13759  fzosplitsni  13782  elfzr  13784  elfzlmr  13785  hashnn0pnf  14352  hashf1lem2  14466  hash2pwpr  14486  pr2pwpr  14489  ccatrn  14600  cats1un  14731  fsumsplit  15751  sumsplit  15778  fprodsplit  15979  rpnnen2lem12  16240  sumeven  16404  sumodd  16405  saddisjlem  16481  lcmfunsnlem1  16654  lcmfunsnlem2lem1  16655  lcmfunsnlem2lem2  16656  lcmfunsnlem2  16657  coprmprod  16678  coprmproddvdslem  16679  nnnn0modprm0  16825  prm23lt5  16833  vdwapun  16993  ramubcl  17037  basprssdmsets  17240  mreexmrid  17658  lubun  18530  chnccats1  18640  smndex1basss  18925  smndex1mgm  18927  smndex1mndlem  18929  smndex1n0mnd  18932  symgextf1  19444  gsumzsplit  19950  gsumzunsnd  19979  gsumunsnfd  19980  dprddisj2  20064  dmdprdsplit2lem  20070  dmdprdsplit2  20071  dprdsplit  20073  cnfldfun  21418  mplcoe1  22070  mplcoe5  22073  evlslem4  22109  mdetunilem9  22660  maducoeval2  22680  madugsum  22683  clslp  23188  islpi  23189  restntr  23222  pnfnei  23260  mnfnei  23261  iunconn  23468  refun0  23555  xkoptsub  23694  ptunhmeo  23848  fbun  23880  filconn  23923  fixufil  23962  ufildr  23971  alexsubALTlem2  24088  alexsubALTlem3  24089  alexsubALTlem4  24090  tsmssplit  24192  xrtgioo  24847  reconnlem2  24868  iccpnfcnv  24986  iccpnfhmeo  24987  rrxcph  25434  rrxdstprj1  25451  mbfss  25688  mbfmax  25691  itg2splitlem  25790  itg2split  25791  iblss2  25848  itgsplit  25878  limcdif  25918  ellimc2  25919  limcmpt  25925  limcres  25928  limccnp  25933  limccnp2  25934  limcco  25935  rollelem  26031  dvivthlem1  26050  dvne0  26053  lhop  26058  degltlem1  26112  ply1rem  26206  fta1glem2  26209  plypf1  26252  plyaddlem1  26253  plymullem1  26254  plycj  26317  plycjOLD  26319  ofmulrt  26323  taylfval  26399  abelthlem2  26472  abelthlem3  26473  reasinsin  26938  scvxcvx  27027  ppinprm  27193  chtnprm  27195  dchrfi  27296  lgsdir2  27371  2lgslem3  27445  2lgsoddprmlem3  27455  nosepdmlem  27724  sltsun1  27858  sltsun2  27859  addsproplem2  28040  addsuniflem  28071  negsid  28111  mulsproplem9  28194  sltmuls1  28217  sltmuls2  28218  precsexlem9  28285  precsexlem11  28287  ltonold  28331  usgrexmplef  29406  cffldtocusgr  29594  vtxdun  29628  eucrct2eupth  30393  shunssi  31517  atomli  32531  atoml2i  32532  rmoun  32641  rmounid  32642  nelun  32661  suppovss  32833  isoun  32854  fzsplit3  32945  eliccioo  33069  gsumwun  33217  cycpmco2  33274  cyc3co2  33281  cycpmrn  33284  elrgspnlem2  33385  ply1dg3rt0irred  33741  lindsun  33883  lbsdiflsp0  33884  ordtconnlem1  34182  xrge0iifcnv  34191  xrge0iifiso  34193  xrge0iifhom  34195  esumsplit  34311  esumpad2  34314  measvuni  34472  sxbrsigalem0  34529  bnj1138  35048  bnj1137  35254  subfacp1lem4  35497  subfacp1lem5  35498  kur14lem7  35526  satfvsucsuc  35679  satfrnmapom  35684  satf0op  35691  satf0n0  35692  sat1el2xp  35693  fmlafvel  35699  isfmlasuc  35702  fmlaomn0  35704  satfv1fvfmla1  35737  2goelgoanfmla1  35738  mrsubcv  35824  mclsax  35883  brcup  36251  refssfne  36682  ttciunun  36835  bj-eltag  37426  bj-0eltag  37427  bj-sngltag  37432  bj-projun  37443  bj-axbun  37485  bj-axadj  37490  bj-imdirco  37646  tan2h  38075  poimirlem2  38085  poimirlem8  38091  poimirlem18  38101  poimirlem21  38104  poimirlem22  38105  poimirlem23  38106  poimirlem24  38107  poimirlem25  38108  poimirlem27  38110  poimirlem29  38112  poimirlem31  38114  poimirlem32  38115  ftc1anclem1  38156  ftc1anclem5  38160  dvasin  38167  dvacos  38168  smprngopr  38515  dfsucmap3  38926  elpadd  40387  paddval0  40398  hdmaplem4  42362  mapdh9a  42377  unitscyglem2  42777  ofun  42818  lzunuz  43313  jm2.23  43537  unxpwdom3  43636  hbtlem5  43669  fzunt  43995  fzuntd  43996  fzunt1d  43997  fzuntgd  43998  rp-fakeinunass  44055  sqrtcvallem1  44171  frege133d  44305  frege83  44486  frege131  44534  frege133  44536  uneqsn  44565  clsk1indlem3  44583  ntrneixb  44635  ntrneix3  44637  ntrneix13  44639  radcnvrat  44854  bccbc  44885  undif3VD  45421  iunconnlem2  45474  permaxinf2lem  45552  fnchoice  45573  limciccioolb  46161  limcicciooub  46175  icccncfext  46425  cncfiooicclem1  46431  fourierdlem70  46714  fourierdlem80  46724  fourierdlem93  46737  fourierdlem101  46745  sge0split  46947  el1fzopredsuc  47884  iccpartltu  47995  iccpartgtl  47996  iccpartgt  47997  iccpartleu  47998  iccpartgel  47999  fmtno4prmfac  48145  31prm  48170  sbgoldbo  48373  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  wtgoldbnnsum4prm  48388  bgoldbnnsum3prm  48390  bgoldbtbndlem3  48393  bgoldbtbnd  48395  elclnbgrelnbgr  48411  clnbgrel  48414  clnbupgrel  48420  dfclnbgr6  48442  isubgr3stgrlem4  48555  usgrexmpl1tri  48611  usgrexmpl2nb0  48617  usgrexmpl2nb1  48618  usgrexmpl2nb2  48619  usgrexmpl2nb3  48620  usgrexmpl2nb4  48621  usgrexmpl2nb5  48622  usgrexmpl2trifr  48623  gpgprismgr4cycllem3  48683  gpgprismgr4cycllem7  48687  gpgprismgr4cycllem10  48690