Theorem elun 4162

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

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1536   ∈ wcel 2105  Vcvv 3477   ∪ cun 3960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967

This theorem is referenced by:  elunnel1  4163  elunnel2  4164  uneqri  4165  uncom  4167  uneq1  4170  nfun  4179  unass  4181  ssun1  4187  elunant  4193  unss1  4194  ssequn1  4195  rexun  4205  elsymdif  4263  indi  4289  undi  4290  unineq  4293  undif3  4305  rabun2  4329  reuun2  4330  undif4  4472  ssundif  4493  dfpr2  4650  elunsn  4687  elpwunsn  4688  eltpg  4690  el7g  4694  pwpr  4905  pwtp  4906  uniun  4934  iinun2  5077  iunun  5097  iunxun  5098  iinuni  5102  brun  5198  pwssun  5579  opthprc  5752  xpundi  5756  xpundir  5757  difxp  6185  sossfld  6207  elsuci  6452  elsucg  6453  elsuc2g  6454  funun  6613  mptun  6714  unima  6983  eqfnun  7056  unpreima  7082  sucexeloniOLD  7829  suceloniOLD  7831  ordsucun  7844  fnse  8156  xpord2pred  8168  xpord3pred  8175  suppofssd  8226  reldmtpos  8257  dftpos4  8268  tpostpos  8269  frrlem12  8320  frrlem13  8321  wfrlem14OLD  8360  wfrlem15OLD  8361  oarec  8598  brdom2  9020  unfi  9209  unxpdomlem3  9285  domunfican  9358  dfsup2  9481  wemapso2lem  9589  unwdomg  9621  unxpwdom2  9625  cantnfp1lem3  9717  rankunb  9887  djur  9956  djuunxp  9958  eldju2ndl  9961  eldju2ndr  9962  djuun  9963  iscard3  10130  kmlem2  10189  ssfin4  10347  dffin7-2  10435  fin1a2lem11  10447  fin1a2lem12  10448  cfpwsdom  10621  elgch  10659  fpwwe2lem12  10679  canthp1lem2  10690  gch2  10712  elnn0  12525  un0addcl  12556  un0mulcl  12557  elxnn0  12598  ltxr  13154  elxr  13155  xrsupexmnf  13343  xrinfmexpnf  13344  supxrun  13354  ixxun  13399  difreicc  13520  iccsplit  13521  fzsplit2  13585  elfzp1  13610  uzsplit  13632  elfzp12  13639  fzosplit  13728  fzouzsplit  13730  elfzonlteqm1  13776  elfzo0l  13791  fzosplitsni  13813  elfzr  13815  elfzlmr  13816  hashnn0pnf  14377  hashf1lem2  14491  hash2pwpr  14511  pr2pwpr  14514  ccatrn  14623  cats1un  14755  fsumsplit  15773  sumsplit  15800  fprodsplit  15998  rpnnen2lem12  16257  sumeven  16420  sumodd  16421  saddisjlem  16497  lcmfunsnlem1  16670  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  lcmfunsnlem2  16673  coprmprod  16694  coprmproddvdslem  16695  nnnn0modprm0  16839  prm23lt5  16847  vdwapun  17007  ramubcl  17051  basprssdmsets  17257  mreexmrid  17687  lubun  18572  smndex1basss  18930  smndex1mgm  18932  smndex1mndlem  18934  smndex1n0mnd  18937  symgextf1  19453  gsumzsplit  19959  gsumzunsnd  19988  gsumunsnfd  19989  dprddisj2  20073  dmdprdsplit2lem  20079  dmdprdsplit2  20080  dprdsplit  20082  cnfldfun  21395  cnfldfunOLD  21408  mplcoe1  22072  mplcoe5  22075  evlslem4  22117  mdetunilem9  22641  maducoeval2  22661  madugsum  22664  clslp  23171  islpi  23172  restntr  23205  pnfnei  23243  mnfnei  23244  iunconn  23451  refun0  23538  xkoptsub  23677  ptunhmeo  23831  fbun  23863  filconn  23906  fixufil  23945  ufildr  23954  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  tsmssplit  24175  xrtgioo  24841  reconnlem2  24862  iccpnfcnv  24988  iccpnfhmeo  24989  rrxcph  25439  rrxdstprj1  25456  mbfss  25694  mbfmax  25697  itg2splitlem  25797  itg2split  25798  iblss2  25855  itgsplit  25885  limcdif  25925  ellimc2  25926  limcmpt  25932  limcres  25935  limccnp  25940  limccnp2  25941  limcco  25942  rollelem  26041  dvivthlem1  26061  dvne0  26064  lhop  26069  degltlem1  26125  ply1rem  26219  fta1glem2  26222  plypf1  26265  plyaddlem1  26266  plymullem1  26267  plycj  26331  plycjOLD  26333  ofmulrt  26337  taylfval  26414  abelthlem2  26490  abelthlem3  26491  reasinsin  26953  scvxcvx  27043  ppinprm  27209  chtnprm  27211  dchrfi  27313  lgsdir2  27388  2lgslem3  27462  2lgsoddprmlem3  27472  nosepdmlem  27742  ssltun1  27867  ssltun2  27868  addsproplem2  28017  addsuniflem  28048  negsid  28087  mulsproplem9  28164  ssltmul1  28187  ssltmul2  28188  precsexlem9  28253  precsexlem11  28255  sltonold  28297  usgrexmplef  29290  cffldtocusgr  29478  cffldtocusgrOLD  29479  vtxdun  29513  eucrct2eupth  30273  shunssi  31396  atomli  32410  atoml2i  32411  rmoun  32521  rmounid  32522  nelun  32540  suppovss  32695  isoun  32716  fzsplit3  32801  eliccioo  32897  gsumwun  33050  cycpmco2  33135  cyc3co2  33142  cycpmrn  33145  elrgspnlem2  33232  ply1dg3rt0irred  33586  lindsun  33652  lbsdiflsp0  33653  ordtconnlem1  33884  xrge0iifcnv  33893  xrge0iifiso  33895  xrge0iifhom  33897  esumsplit  34033  esumpad2  34036  measvuni  34194  sxbrsigalem0  34252  bnj1138  34780  bnj1137  34987  subfacp1lem4  35167  subfacp1lem5  35168  kur14lem7  35196  satfvsucsuc  35349  satfrnmapom  35354  satf0op  35361  satf0n0  35362  sat1el2xp  35363  fmlafvel  35369  isfmlasuc  35372  fmlaomn0  35374  satfv1fvfmla1  35407  2goelgoanfmla1  35408  mrsubcv  35494  mclsax  35553  brcup  35920  refssfne  36340  bj-eltag  36959  bj-0eltag  36960  bj-sngltag  36965  bj-projun  36976  bj-axbun  37018  bj-axadj  37023  bj-imdirco  37172  tan2h  37598  poimirlem2  37608  poimirlem8  37614  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem27  37633  poimirlem29  37635  poimirlem31  37637  poimirlem32  37638  ftc1anclem1  37679  ftc1anclem5  37683  dvasin  37690  dvacos  37691  smprngopr  38038  elpadd  39781  paddval0  39792  hdmaplem4  41756  mapdh9a  41771  unitscyglem2  42177  ofun  42255  lzunuz  42755  jm2.23  42984  unxpwdom3  43083  hbtlem5  43116  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  rp-fakeinunass  43504  sqrtcvallem1  43620  frege133d  43754  frege83  43935  frege131  43983  frege133  43985  uneqsn  44014  clsk1indlem3  44032  ntrneixb  44084  ntrneix3  44086  ntrneix13  44088  radcnvrat  44309  bccbc  44340  undif3VD  44879  iunconnlem2  44932  fnchoice  44966  limciccioolb  45576  limcicciooub  45592  icccncfext  45842  cncfiooicclem1  45848  fourierdlem70  46131  fourierdlem80  46141  fourierdlem93  46154  fourierdlem101  46162  sge0split  46364  el1fzopredsuc  47274  iccpartltu  47349  iccpartgtl  47350  iccpartgt  47351  iccpartleu  47352  iccpartgel  47353  fmtno4prmfac  47496  31prm  47521  sbgoldbo  47711  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  bgoldbtbndlem3  47731  bgoldbtbnd  47733  elclnbgrelnbgr  47749  clnbgrel  47752  clnbupgrel  47758  dfclnbgr6  47779  isubgr3stgrlem4  47871  usgrexmpl1tri  47919  usgrexmpl2nb0  47925  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  usgrexmpl2trifr  47931