Theorem elun 4107

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

Syntax hints:   ↔ wb 206   ∨ wo 848   = wceq 1542   ∈ wcel 2114  Vcvv 3442   ∪ cun 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908

This theorem is referenced by:  elunnel1  4108  elunnel2  4109  uneqri  4110  uncom  4112  uneq1  4115  nfun  4124  unass  4126  ssun1  4132  elunant  4138  unss1  4139  ssequn1  4140  rexun  4150  elsymdif  4212  indi  4238  undi  4239  unineq  4242  undif3  4254  rabun2  4278  reuun2  4279  undif4  4421  ssundif  4442  dfpr2  4603  elunsn  4642  elpwunsn  4643  eltpg  4645  el7g  4649  pwpr  4859  pwtp  4860  uniun  4888  iinun2  5030  iunun  5050  iunxun  5051  iinuni  5055  brun  5151  pwssun  5524  opthprc  5696  xpundi  5701  xpundir  5702  imadifssran  6117  difxp  6130  sossfld  6152  elsuci  6394  elsucg  6395  elsuc2g  6396  funun  6546  mptun  6646  unima  6917  eqfnun  6991  unpreima  7017  ordsucun  7777  resf1extb  7886  fnse  8085  xpord2pred  8097  xpord3pred  8104  suppofssd  8155  reldmtpos  8186  dftpos4  8197  tpostpos  8198  frrlem12  8249  frrlem13  8250  oarec  8499  brdom2  8931  unfi  9107  unxpdomlem3  9170  domunfican  9234  dfsup2  9359  wemapso2lem  9469  unwdomg  9501  unxpwdom2  9505  cantnfp1lem3  9601  rankunb  9774  djur  9843  djuunxp  9845  eldju2ndl  9848  eldju2ndr  9849  djuun  9850  iscard3  10015  kmlem2  10074  ssfin4  10232  dffin7-2  10320  fin1a2lem11  10332  fin1a2lem12  10333  cfpwsdom  10507  elgch  10545  fpwwe2lem12  10565  canthp1lem2  10576  gch2  10598  elnn0  12415  un0addcl  12446  un0mulcl  12447  elxnn0  12488  ltxr  13041  elxr  13042  xrsupexmnf  13232  xrinfmexpnf  13233  supxrun  13243  ixxun  13289  difreicc  13412  iccsplit  13413  fzsplit2  13477  elfzp1  13502  uzsplit  13524  elfzp12  13531  fzosplit  13620  fzouzsplit  13622  elfzonlteqm1  13669  elfzo0l  13684  fzosplitsni  13707  elfzr  13709  elfzlmr  13710  hashnn0pnf  14277  hashf1lem2  14391  hash2pwpr  14411  pr2pwpr  14414  ccatrn  14525  cats1un  14656  fsumsplit  15676  sumsplit  15703  fprodsplit  15901  rpnnen2lem12  16162  sumeven  16326  sumodd  16327  saddisjlem  16403  lcmfunsnlem1  16576  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  lcmfunsnlem2  16579  coprmprod  16600  coprmproddvdslem  16601  nnnn0modprm0  16746  prm23lt5  16754  vdwapun  16914  ramubcl  16958  basprssdmsets  17160  mreexmrid  17578  lubun  18450  chnccats1  18560  smndex1basss  18842  smndex1mgm  18844  smndex1mndlem  18846  smndex1n0mnd  18849  symgextf1  19362  gsumzsplit  19868  gsumzunsnd  19897  gsumunsnfd  19898  dprddisj2  19982  dmdprdsplit2lem  19988  dmdprdsplit2  19989  dprdsplit  19991  cnfldfun  21335  cnfldfunOLD  21348  mplcoe1  22004  mplcoe5  22007  evlslem4  22043  mdetunilem9  22576  maducoeval2  22596  madugsum  22599  clslp  23104  islpi  23105  restntr  23138  pnfnei  23176  mnfnei  23177  iunconn  23384  refun0  23471  xkoptsub  23610  ptunhmeo  23764  fbun  23796  filconn  23839  fixufil  23878  ufildr  23887  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALTlem4  24006  tsmssplit  24108  xrtgioo  24763  reconnlem2  24784  iccpnfcnv  24910  iccpnfhmeo  24911  rrxcph  25360  rrxdstprj1  25377  mbfss  25615  mbfmax  25618  itg2splitlem  25717  itg2split  25718  iblss2  25775  itgsplit  25805  limcdif  25845  ellimc2  25846  limcmpt  25852  limcres  25855  limccnp  25860  limccnp2  25861  limcco  25862  rollelem  25961  dvivthlem1  25981  dvne0  25984  lhop  25989  degltlem1  26045  ply1rem  26139  fta1glem2  26142  plypf1  26185  plyaddlem1  26186  plymullem1  26187  plycj  26251  plycjOLD  26253  ofmulrt  26257  taylfval  26334  abelthlem2  26410  abelthlem3  26411  reasinsin  26874  scvxcvx  26964  ppinprm  27130  chtnprm  27132  dchrfi  27234  lgsdir2  27309  2lgslem3  27383  2lgsoddprmlem3  27393  nosepdmlem  27663  sltsun1  27796  sltsun2  27797  addsproplem2  27978  addsuniflem  28009  negsid  28049  mulsproplem9  28132  sltmuls1  28155  sltmuls2  28156  precsexlem9  28223  precsexlem11  28225  ltonold  28269  usgrexmplef  29344  cffldtocusgr  29532  cffldtocusgrOLD  29533  vtxdun  29567  eucrct2eupth  30332  shunssi  31455  atomli  32469  atoml2i  32470  rmoun  32579  rmounid  32580  nelun  32599  suppovss  32770  isoun  32791  fzsplit3  32883  eliccioo  33022  gsumwun  33169  cycpmco2  33226  cyc3co2  33233  cycpmrn  33236  elrgspnlem2  33336  ply1dg3rt0irred  33676  lindsun  33802  lbsdiflsp0  33803  ordtconnlem1  34101  xrge0iifcnv  34110  xrge0iifiso  34112  xrge0iifhom  34114  esumsplit  34230  esumpad2  34233  measvuni  34391  sxbrsigalem0  34448  bnj1138  34964  bnj1137  35170  subfacp1lem4  35396  subfacp1lem5  35397  kur14lem7  35425  satfvsucsuc  35578  satfrnmapom  35583  satf0op  35590  satf0n0  35591  sat1el2xp  35592  fmlafvel  35598  isfmlasuc  35601  fmlaomn0  35603  satfv1fvfmla1  35636  2goelgoanfmla1  35637  mrsubcv  35723  mclsax  35782  brcup  36150  refssfne  36571  bj-eltag  37219  bj-0eltag  37220  bj-sngltag  37225  bj-projun  37236  bj-axbun  37278  bj-axadj  37283  bj-imdirco  37439  tan2h  37857  poimirlem2  37867  poimirlem8  37873  poimirlem18  37883  poimirlem21  37886  poimirlem22  37887  poimirlem23  37888  poimirlem24  37889  poimirlem25  37890  poimirlem27  37892  poimirlem29  37894  poimirlem31  37896  poimirlem32  37897  ftc1anclem1  37938  ftc1anclem5  37942  dvasin  37949  dvacos  37950  smprngopr  38297  dfsucmap3  38708  elpadd  40169  paddval0  40180  hdmaplem4  42144  mapdh9a  42159  unitscyglem2  42560  ofun  42602  lzunuz  43119  jm2.23  43347  unxpwdom3  43446  hbtlem5  43479  fzunt  43805  fzuntd  43806  fzunt1d  43807  fzuntgd  43808  rp-fakeinunass  43865  sqrtcvallem1  43981  frege133d  44115  frege83  44296  frege131  44344  frege133  44346  uneqsn  44375  clsk1indlem3  44393  ntrneixb  44445  ntrneix3  44447  ntrneix13  44449  radcnvrat  44664  bccbc  44695  undif3VD  45231  iunconnlem2  45284  permaxinf2lem  45362  fnchoice  45383  limciccioolb  45975  limcicciooub  45989  icccncfext  46239  cncfiooicclem1  46245  fourierdlem70  46528  fourierdlem80  46538  fourierdlem93  46551  fourierdlem101  46559  sge0split  46761  el1fzopredsuc  47679  iccpartltu  47779  iccpartgtl  47780  iccpartgt  47781  iccpartleu  47782  iccpartgel  47783  fmtno4prmfac  47926  31prm  47951  sbgoldbo  48141  nnsum4primeseven  48154  nnsum4primesevenALTV  48155  wtgoldbnnsum4prm  48156  bgoldbnnsum3prm  48158  bgoldbtbndlem3  48161  bgoldbtbnd  48163  elclnbgrelnbgr  48179  clnbgrel  48182  clnbupgrel  48188  dfclnbgr6  48210  isubgr3stgrlem4  48323  usgrexmpl1tri  48379  usgrexmpl2nb0  48385  usgrexmpl2nb1  48386  usgrexmpl2nb2  48387  usgrexmpl2nb3  48388  usgrexmpl2nb4  48389  usgrexmpl2nb5  48390  usgrexmpl2trifr  48391  gpgprismgr4cycllem3  48451  gpgprismgr4cycllem7  48455  gpgprismgr4cycllem10  48458