Theorem elun 4119

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 3471	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3471	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3471	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 857	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2817	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2817	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 918	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3922	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3650	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1540   ∈ wcel 2109  Vcvv 3450   ∪ cun 3915

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922

This theorem is referenced by:  elunnel1  4120  elunnel2  4121  uneqri  4122  uncom  4124  uneq1  4127  nfun  4136  unass  4138  ssun1  4144  elunant  4150  unss1  4151  ssequn1  4152  rexun  4162  elsymdif  4224  indi  4250  undi  4251  unineq  4254  undif3  4266  rabun2  4290  reuun2  4291  undif4  4433  ssundif  4454  dfpr2  4613  elunsn  4650  elpwunsn  4651  eltpg  4653  el7g  4657  pwpr  4868  pwtp  4869  uniun  4897  iinun2  5040  iunun  5060  iunxun  5061  iinuni  5065  brun  5161  pwssun  5533  opthprc  5705  xpundi  5710  xpundir  5711  imadifssran  6127  difxp  6140  sossfld  6162  elsuci  6404  elsucg  6405  elsuc2g  6406  funun  6565  mptun  6667  unima  6939  eqfnun  7012  unpreima  7038  sucexeloniOLD  7789  ordsucun  7803  resf1extb  7913  fnse  8115  xpord2pred  8127  xpord3pred  8134  suppofssd  8185  reldmtpos  8216  dftpos4  8227  tpostpos  8228  frrlem12  8279  frrlem13  8280  oarec  8529  brdom2  8956  unfi  9141  unxpdomlem3  9206  domunfican  9279  dfsup2  9402  wemapso2lem  9512  unwdomg  9544  unxpwdom2  9548  cantnfp1lem3  9640  rankunb  9810  djur  9879  djuunxp  9881  eldju2ndl  9884  eldju2ndr  9885  djuun  9886  iscard3  10053  kmlem2  10112  ssfin4  10270  dffin7-2  10358  fin1a2lem11  10370  fin1a2lem12  10371  cfpwsdom  10544  elgch  10582  fpwwe2lem12  10602  canthp1lem2  10613  gch2  10635  elnn0  12451  un0addcl  12482  un0mulcl  12483  elxnn0  12524  ltxr  13082  elxr  13083  xrsupexmnf  13272  xrinfmexpnf  13273  supxrun  13283  ixxun  13329  difreicc  13452  iccsplit  13453  fzsplit2  13517  elfzp1  13542  uzsplit  13564  elfzp12  13571  fzosplit  13660  fzouzsplit  13662  elfzonlteqm1  13709  elfzo0l  13724  fzosplitsni  13746  elfzr  13748  elfzlmr  13749  hashnn0pnf  14314  hashf1lem2  14428  hash2pwpr  14448  pr2pwpr  14451  ccatrn  14561  cats1un  14693  fsumsplit  15714  sumsplit  15741  fprodsplit  15939  rpnnen2lem12  16200  sumeven  16364  sumodd  16365  saddisjlem  16441  lcmfunsnlem1  16614  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  lcmfunsnlem2  16617  coprmprod  16638  coprmproddvdslem  16639  nnnn0modprm0  16784  prm23lt5  16792  vdwapun  16952  ramubcl  16996  basprssdmsets  17198  mreexmrid  17611  lubun  18481  smndex1basss  18839  smndex1mgm  18841  smndex1mndlem  18843  smndex1n0mnd  18846  symgextf1  19358  gsumzsplit  19864  gsumzunsnd  19893  gsumunsnfd  19894  dprddisj2  19978  dmdprdsplit2lem  19984  dmdprdsplit2  19985  dprdsplit  19987  cnfldfun  21285  cnfldfunOLD  21298  mplcoe1  21951  mplcoe5  21954  evlslem4  21990  mdetunilem9  22514  maducoeval2  22534  madugsum  22537  clslp  23042  islpi  23043  restntr  23076  pnfnei  23114  mnfnei  23115  iunconn  23322  refun0  23409  xkoptsub  23548  ptunhmeo  23702  fbun  23734  filconn  23777  fixufil  23816  ufildr  23825  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  tsmssplit  24046  xrtgioo  24702  reconnlem2  24723  iccpnfcnv  24849  iccpnfhmeo  24850  rrxcph  25299  rrxdstprj1  25316  mbfss  25554  mbfmax  25557  itg2splitlem  25656  itg2split  25657  iblss2  25714  itgsplit  25744  limcdif  25784  ellimc2  25785  limcmpt  25791  limcres  25794  limccnp  25799  limccnp2  25800  limcco  25801  rollelem  25900  dvivthlem1  25920  dvne0  25923  lhop  25928  degltlem1  25984  ply1rem  26078  fta1glem2  26081  plypf1  26124  plyaddlem1  26125  plymullem1  26126  plycj  26190  plycjOLD  26192  ofmulrt  26196  taylfval  26273  abelthlem2  26349  abelthlem3  26350  reasinsin  26813  scvxcvx  26903  ppinprm  27069  chtnprm  27071  dchrfi  27173  lgsdir2  27248  2lgslem3  27322  2lgsoddprmlem3  27332  nosepdmlem  27602  ssltun1  27727  ssltun2  27728  addsproplem2  27884  addsuniflem  27915  negsid  27954  mulsproplem9  28034  ssltmul1  28057  ssltmul2  28058  precsexlem9  28124  precsexlem11  28126  sltonold  28169  usgrexmplef  29193  cffldtocusgr  29381  cffldtocusgrOLD  29382  vtxdun  29416  eucrct2eupth  30181  shunssi  31304  atomli  32318  atoml2i  32319  rmoun  32430  rmounid  32431  nelun  32449  suppovss  32611  isoun  32632  fzsplit3  32723  eliccioo  32858  chnccats1  32948  gsumwun  33012  cycpmco2  33097  cyc3co2  33104  cycpmrn  33107  elrgspnlem2  33201  ply1dg3rt0irred  33558  lindsun  33628  lbsdiflsp0  33629  ordtconnlem1  33921  xrge0iifcnv  33930  xrge0iifiso  33932  xrge0iifhom  33934  esumsplit  34050  esumpad2  34053  measvuni  34211  sxbrsigalem0  34269  bnj1138  34785  bnj1137  34992  subfacp1lem4  35177  subfacp1lem5  35178  kur14lem7  35206  satfvsucsuc  35359  satfrnmapom  35364  satf0op  35371  satf0n0  35372  sat1el2xp  35373  fmlafvel  35379  isfmlasuc  35382  fmlaomn0  35384  satfv1fvfmla1  35417  2goelgoanfmla1  35418  mrsubcv  35504  mclsax  35563  brcup  35934  refssfne  36353  bj-eltag  36972  bj-0eltag  36973  bj-sngltag  36978  bj-projun  36989  bj-axbun  37031  bj-axadj  37036  bj-imdirco  37185  tan2h  37613  poimirlem2  37623  poimirlem8  37629  poimirlem18  37639  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem27  37648  poimirlem29  37650  poimirlem31  37652  poimirlem32  37653  ftc1anclem1  37694  ftc1anclem5  37698  dvasin  37705  dvacos  37706  smprngopr  38053  elpadd  39800  paddval0  39811  hdmaplem4  41775  mapdh9a  41790  unitscyglem2  42191  ofun  42231  lzunuz  42763  jm2.23  42992  unxpwdom3  43091  hbtlem5  43124  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  rp-fakeinunass  43511  sqrtcvallem1  43627  frege133d  43761  frege83  43942  frege131  43990  frege133  43992  uneqsn  44021  clsk1indlem3  44039  ntrneixb  44091  ntrneix3  44093  ntrneix13  44095  radcnvrat  44310  bccbc  44341  undif3VD  44878  iunconnlem2  44931  permaxinf2lem  45009  fnchoice  45030  limciccioolb  45626  limcicciooub  45642  icccncfext  45892  cncfiooicclem1  45898  fourierdlem70  46181  fourierdlem80  46191  fourierdlem93  46204  fourierdlem101  46212  sge0split  46414  el1fzopredsuc  47330  iccpartltu  47430  iccpartgtl  47431  iccpartgt  47432  iccpartleu  47433  iccpartgel  47434  fmtno4prmfac  47577  31prm  47602  sbgoldbo  47792  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  bgoldbtbndlem3  47812  bgoldbtbnd  47814  elclnbgrelnbgr  47830  clnbgrel  47833  clnbupgrel  47839  dfclnbgr6  47860  isubgr3stgrlem4  47972  usgrexmpl1tri  48020  usgrexmpl2nb0  48026  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  usgrexmpl2trifr  48032  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem10  48098