Theorem elun 4105

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

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1541   ∈ wcel 2113  Vcvv 3440   ∪ cun 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906

This theorem is referenced by:  elunnel1  4106  elunnel2  4107  uneqri  4108  uncom  4110  uneq1  4113  nfun  4122  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  4419  ssundif  4440  dfpr2  4601  elunsn  4640  elpwunsn  4641  eltpg  4643  el7g  4647  pwpr  4857  pwtp  4858  uniun  4886  iinun2  5028  iunun  5048  iunxun  5049  iinuni  5053  brun  5149  pwssun  5516  opthprc  5688  xpundi  5693  xpundir  5694  imadifssran  6109  difxp  6122  sossfld  6144  elsuci  6386  elsucg  6387  elsuc2g  6388  funun  6538  mptun  6638  unima  6909  eqfnun  6982  unpreima  7008  ordsucun  7767  resf1extb  7876  fnse  8075  xpord2pred  8087  xpord3pred  8094  suppofssd  8145  reldmtpos  8176  dftpos4  8187  tpostpos  8188  frrlem12  8239  frrlem13  8240  oarec  8489  brdom2  8919  unfi  9095  unxpdomlem3  9158  domunfican  9222  dfsup2  9347  wemapso2lem  9457  unwdomg  9489  unxpwdom2  9493  cantnfp1lem3  9589  rankunb  9762  djur  9831  djuunxp  9833  eldju2ndl  9836  eldju2ndr  9837  djuun  9838  iscard3  10003  kmlem2  10062  ssfin4  10220  dffin7-2  10308  fin1a2lem11  10320  fin1a2lem12  10321  cfpwsdom  10495  elgch  10533  fpwwe2lem12  10553  canthp1lem2  10564  gch2  10586  elnn0  12403  un0addcl  12434  un0mulcl  12435  elxnn0  12476  ltxr  13029  elxr  13030  xrsupexmnf  13220  xrinfmexpnf  13221  supxrun  13231  ixxun  13277  difreicc  13400  iccsplit  13401  fzsplit2  13465  elfzp1  13490  uzsplit  13512  elfzp12  13519  fzosplit  13608  fzouzsplit  13610  elfzonlteqm1  13657  elfzo0l  13672  fzosplitsni  13695  elfzr  13697  elfzlmr  13698  hashnn0pnf  14265  hashf1lem2  14379  hash2pwpr  14399  pr2pwpr  14402  ccatrn  14513  cats1un  14644  fsumsplit  15664  sumsplit  15691  fprodsplit  15889  rpnnen2lem12  16150  sumeven  16314  sumodd  16315  saddisjlem  16391  lcmfunsnlem1  16564  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  lcmfunsnlem2  16567  coprmprod  16588  coprmproddvdslem  16589  nnnn0modprm0  16734  prm23lt5  16742  vdwapun  16902  ramubcl  16946  basprssdmsets  17148  mreexmrid  17566  lubun  18438  chnccats1  18548  smndex1basss  18830  smndex1mgm  18832  smndex1mndlem  18834  smndex1n0mnd  18837  symgextf1  19350  gsumzsplit  19856  gsumzunsnd  19885  gsumunsnfd  19886  dprddisj2  19970  dmdprdsplit2lem  19976  dmdprdsplit2  19977  dprdsplit  19979  cnfldfun  21323  cnfldfunOLD  21336  mplcoe1  21992  mplcoe5  21995  evlslem4  22031  mdetunilem9  22564  maducoeval2  22584  madugsum  22587  clslp  23092  islpi  23093  restntr  23126  pnfnei  23164  mnfnei  23165  iunconn  23372  refun0  23459  xkoptsub  23598  ptunhmeo  23752  fbun  23784  filconn  23827  fixufil  23866  ufildr  23875  alexsubALTlem2  23992  alexsubALTlem3  23993  alexsubALTlem4  23994  tsmssplit  24096  xrtgioo  24751  reconnlem2  24772  iccpnfcnv  24898  iccpnfhmeo  24899  rrxcph  25348  rrxdstprj1  25365  mbfss  25603  mbfmax  25606  itg2splitlem  25705  itg2split  25706  iblss2  25763  itgsplit  25793  limcdif  25833  ellimc2  25834  limcmpt  25840  limcres  25843  limccnp  25848  limccnp2  25849  limcco  25850  rollelem  25949  dvivthlem1  25969  dvne0  25972  lhop  25977  degltlem1  26033  ply1rem  26127  fta1glem2  26130  plypf1  26173  plyaddlem1  26174  plymullem1  26175  plycj  26239  plycjOLD  26241  ofmulrt  26245  taylfval  26322  abelthlem2  26398  abelthlem3  26399  reasinsin  26862  scvxcvx  26952  ppinprm  27118  chtnprm  27120  dchrfi  27222  lgsdir2  27297  2lgslem3  27371  2lgsoddprmlem3  27381  nosepdmlem  27651  sltsun1  27784  sltsun2  27785  addsproplem2  27966  addsuniflem  27997  negsid  28037  mulsproplem9  28120  sltmuls1  28143  sltmuls2  28144  precsexlem9  28211  precsexlem11  28213  ltonold  28257  usgrexmplef  29332  cffldtocusgr  29520  cffldtocusgrOLD  29521  vtxdun  29555  eucrct2eupth  30320  shunssi  31443  atomli  32457  atoml2i  32458  rmoun  32568  rmounid  32569  nelun  32588  suppovss  32760  isoun  32781  fzsplit3  32873  eliccioo  33012  gsumwun  33158  cycpmco2  33215  cyc3co2  33222  cycpmrn  33225  elrgspnlem2  33325  ply1dg3rt0irred  33665  lindsun  33782  lbsdiflsp0  33783  ordtconnlem1  34081  xrge0iifcnv  34090  xrge0iifiso  34092  xrge0iifhom  34094  esumsplit  34210  esumpad2  34213  measvuni  34371  sxbrsigalem0  34428  bnj1138  34944  bnj1137  35151  subfacp1lem4  35377  subfacp1lem5  35378  kur14lem7  35406  satfvsucsuc  35559  satfrnmapom  35564  satf0op  35571  satf0n0  35572  sat1el2xp  35573  fmlafvel  35579  isfmlasuc  35582  fmlaomn0  35584  satfv1fvfmla1  35617  2goelgoanfmla1  35618  mrsubcv  35704  mclsax  35763  brcup  36131  refssfne  36552  bj-eltag  37178  bj-0eltag  37179  bj-sngltag  37184  bj-projun  37195  bj-axbun  37237  bj-axadj  37242  bj-imdirco  37391  tan2h  37809  poimirlem2  37819  poimirlem8  37825  poimirlem18  37835  poimirlem21  37838  poimirlem22  37839  poimirlem23  37840  poimirlem24  37841  poimirlem25  37842  poimirlem27  37844  poimirlem29  37846  poimirlem31  37848  poimirlem32  37849  ftc1anclem1  37890  ftc1anclem5  37894  dvasin  37901  dvacos  37902  smprngopr  38249  dfsucmap3  38633  elpadd  40055  paddval0  40066  hdmaplem4  42030  mapdh9a  42045  unitscyglem2  42446  ofun  42488  lzunuz  43006  jm2.23  43234  unxpwdom3  43333  hbtlem5  43366  fzunt  43692  fzuntd  43693  fzunt1d  43694  fzuntgd  43695  rp-fakeinunass  43752  sqrtcvallem1  43868  frege133d  44002  frege83  44183  frege131  44231  frege133  44233  uneqsn  44262  clsk1indlem3  44280  ntrneixb  44332  ntrneix3  44334  ntrneix13  44336  radcnvrat  44551  bccbc  44582  undif3VD  45118  iunconnlem2  45171  permaxinf2lem  45249  fnchoice  45270  limciccioolb  45863  limcicciooub  45877  icccncfext  46127  cncfiooicclem1  46133  fourierdlem70  46416  fourierdlem80  46426  fourierdlem93  46439  fourierdlem101  46447  sge0split  46649  el1fzopredsuc  47567  iccpartltu  47667  iccpartgtl  47668  iccpartgt  47669  iccpartleu  47670  iccpartgel  47671  fmtno4prmfac  47814  31prm  47839  sbgoldbo  48029  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  wtgoldbnnsum4prm  48044  bgoldbnnsum3prm  48046  bgoldbtbndlem3  48049  bgoldbtbnd  48051  elclnbgrelnbgr  48067  clnbgrel  48070  clnbupgrel  48076  dfclnbgr6  48098  isubgr3stgrlem4  48211  usgrexmpl1tri  48267  usgrexmpl2nb0  48273  usgrexmpl2nb1  48274  usgrexmpl2nb2  48275  usgrexmpl2nb3  48276  usgrexmpl2nb4  48277  usgrexmpl2nb5  48278  usgrexmpl2trifr  48279  gpgprismgr4cycllem3  48339  gpgprismgr4cycllem7  48343  gpgprismgr4cycllem10  48346