Theorem elun 4153

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

Syntax hints:   ↔ wb 206   ∨ wo 848   = wceq 1540   ∈ wcel 2108  Vcvv 3480   ∪ cun 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956

This theorem is referenced by:  elunnel1  4154  elunnel2  4155  uneqri  4156  uncom  4158  uneq1  4161  nfun  4170  unass  4172  ssun1  4178  elunant  4184  unss1  4185  ssequn1  4186  rexun  4196  elsymdif  4258  indi  4284  undi  4285  unineq  4288  undif3  4300  rabun2  4324  reuun2  4325  undif4  4467  ssundif  4488  dfpr2  4646  elunsn  4683  elpwunsn  4684  eltpg  4686  el7g  4690  pwpr  4901  pwtp  4902  uniun  4930  iinun2  5073  iunun  5093  iunxun  5094  iinuni  5098  brun  5194  pwssun  5575  opthprc  5749  xpundi  5754  xpundir  5755  imadifssran  6171  difxp  6184  sossfld  6206  elsuci  6451  elsucg  6452  elsuc2g  6453  funun  6612  mptun  6714  unima  6984  eqfnun  7057  unpreima  7083  sucexeloniOLD  7830  suceloniOLD  7832  ordsucun  7845  resf1extb  7956  fnse  8158  xpord2pred  8170  xpord3pred  8177  suppofssd  8228  reldmtpos  8259  dftpos4  8270  tpostpos  8271  frrlem12  8322  frrlem13  8323  wfrlem14OLD  8362  wfrlem15OLD  8363  oarec  8600  brdom2  9022  unfi  9211  unxpdomlem3  9288  domunfican  9361  dfsup2  9484  wemapso2lem  9592  unwdomg  9624  unxpwdom2  9628  cantnfp1lem3  9720  rankunb  9890  djur  9959  djuunxp  9961  eldju2ndl  9964  eldju2ndr  9965  djuun  9966  iscard3  10133  kmlem2  10192  ssfin4  10350  dffin7-2  10438  fin1a2lem11  10450  fin1a2lem12  10451  cfpwsdom  10624  elgch  10662  fpwwe2lem12  10682  canthp1lem2  10693  gch2  10715  elnn0  12528  un0addcl  12559  un0mulcl  12560  elxnn0  12601  ltxr  13157  elxr  13158  xrsupexmnf  13347  xrinfmexpnf  13348  supxrun  13358  ixxun  13403  difreicc  13524  iccsplit  13525  fzsplit2  13589  elfzp1  13614  uzsplit  13636  elfzp12  13643  fzosplit  13732  fzouzsplit  13734  elfzonlteqm1  13780  elfzo0l  13795  fzosplitsni  13817  elfzr  13819  elfzlmr  13820  hashnn0pnf  14381  hashf1lem2  14495  hash2pwpr  14515  pr2pwpr  14518  ccatrn  14627  cats1un  14759  fsumsplit  15777  sumsplit  15804  fprodsplit  16002  rpnnen2lem12  16261  sumeven  16424  sumodd  16425  saddisjlem  16501  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  coprmprod  16698  coprmproddvdslem  16699  nnnn0modprm0  16844  prm23lt5  16852  vdwapun  17012  ramubcl  17056  basprssdmsets  17259  mreexmrid  17686  lubun  18560  smndex1basss  18918  smndex1mgm  18920  smndex1mndlem  18922  smndex1n0mnd  18925  symgextf1  19439  gsumzsplit  19945  gsumzunsnd  19974  gsumunsnfd  19975  dprddisj2  20059  dmdprdsplit2lem  20065  dmdprdsplit2  20066  dprdsplit  20068  cnfldfun  21378  cnfldfunOLD  21391  mplcoe1  22055  mplcoe5  22058  evlslem4  22100  mdetunilem9  22626  maducoeval2  22646  madugsum  22649  clslp  23156  islpi  23157  restntr  23190  pnfnei  23228  mnfnei  23229  iunconn  23436  refun0  23523  xkoptsub  23662  ptunhmeo  23816  fbun  23848  filconn  23891  fixufil  23930  ufildr  23939  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  tsmssplit  24160  xrtgioo  24828  reconnlem2  24849  iccpnfcnv  24975  iccpnfhmeo  24976  rrxcph  25426  rrxdstprj1  25443  mbfss  25681  mbfmax  25684  itg2splitlem  25783  itg2split  25784  iblss2  25841  itgsplit  25871  limcdif  25911  ellimc2  25912  limcmpt  25918  limcres  25921  limccnp  25926  limccnp2  25927  limcco  25928  rollelem  26027  dvivthlem1  26047  dvne0  26050  lhop  26055  degltlem1  26111  ply1rem  26205  fta1glem2  26208  plypf1  26251  plyaddlem1  26252  plymullem1  26253  plycj  26317  plycjOLD  26319  ofmulrt  26323  taylfval  26400  abelthlem2  26476  abelthlem3  26477  reasinsin  26939  scvxcvx  27029  ppinprm  27195  chtnprm  27197  dchrfi  27299  lgsdir2  27374  2lgslem3  27448  2lgsoddprmlem3  27458  nosepdmlem  27728  ssltun1  27853  ssltun2  27854  addsproplem2  28003  addsuniflem  28034  negsid  28073  mulsproplem9  28150  ssltmul1  28173  ssltmul2  28174  precsexlem9  28239  precsexlem11  28241  sltonold  28283  usgrexmplef  29276  cffldtocusgr  29464  cffldtocusgrOLD  29465  vtxdun  29499  eucrct2eupth  30264  shunssi  31387  atomli  32401  atoml2i  32402  rmoun  32513  rmounid  32514  nelun  32532  suppovss  32690  isoun  32711  fzsplit3  32795  eliccioo  32913  chnccats1  33005  gsumwun  33068  cycpmco2  33153  cyc3co2  33160  cycpmrn  33163  elrgspnlem2  33247  ply1dg3rt0irred  33607  lindsun  33676  lbsdiflsp0  33677  ordtconnlem1  33923  xrge0iifcnv  33932  xrge0iifiso  33934  xrge0iifhom  33936  esumsplit  34054  esumpad2  34057  measvuni  34215  sxbrsigalem0  34273  bnj1138  34802  bnj1137  35009  subfacp1lem4  35188  subfacp1lem5  35189  kur14lem7  35217  satfvsucsuc  35370  satfrnmapom  35375  satf0op  35382  satf0n0  35383  sat1el2xp  35384  fmlafvel  35390  isfmlasuc  35393  fmlaomn0  35395  satfv1fvfmla1  35428  2goelgoanfmla1  35429  mrsubcv  35515  mclsax  35574  brcup  35940  refssfne  36359  bj-eltag  36978  bj-0eltag  36979  bj-sngltag  36984  bj-projun  36995  bj-axbun  37037  bj-axadj  37042  bj-imdirco  37191  tan2h  37619  poimirlem2  37629  poimirlem8  37635  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem27  37654  poimirlem29  37656  poimirlem31  37658  poimirlem32  37659  ftc1anclem1  37700  ftc1anclem5  37704  dvasin  37711  dvacos  37712  smprngopr  38059  elpadd  39801  paddval0  39812  hdmaplem4  41776  mapdh9a  41791  unitscyglem2  42197  ofun  42277  lzunuz  42779  jm2.23  43008  unxpwdom3  43107  hbtlem5  43140  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  rp-fakeinunass  43528  sqrtcvallem1  43644  frege133d  43778  frege83  43959  frege131  44007  frege133  44009  uneqsn  44038  clsk1indlem3  44056  ntrneixb  44108  ntrneix3  44110  ntrneix13  44112  radcnvrat  44333  bccbc  44364  undif3VD  44902  iunconnlem2  44955  fnchoice  45034  limciccioolb  45636  limcicciooub  45652  icccncfext  45902  cncfiooicclem1  45908  fourierdlem70  46191  fourierdlem80  46201  fourierdlem93  46214  fourierdlem101  46222  sge0split  46424  el1fzopredsuc  47337  iccpartltu  47412  iccpartgtl  47413  iccpartgt  47414  iccpartleu  47415  iccpartgel  47416  fmtno4prmfac  47559  31prm  47584  sbgoldbo  47774  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  bgoldbtbndlem3  47794  bgoldbtbnd  47796  elclnbgrelnbgr  47812  clnbgrel  47815  clnbupgrel  47821  dfclnbgr6  47842  isubgr3stgrlem4  47936  usgrexmpl1tri  47984  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  usgrexmpl2trifr  47996