Theorem elun 4100

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 3472	. 2 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) → 𝐴 ∈ V)
2		elex 3472	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		elex 3472	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4	2, 3	jaoi 871	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
5		eleq1 2849	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
6		eleq1 2849	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
7	5, 6	orbi12d 932	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
8		df-un 3904	. . 3 ⊢ (𝐵 ∪ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 3634	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)))
10	1, 4, 9	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   = wceq 1570   ∈ wcel 2145  Vcvv 3451   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904

This theorem is used by:  elunnel1  4101  elunnel2  4102  uneqri  4103  uncom  4105  uneq1  4108  nfun  4117  unass  4118  ssun1  4124  elunant  4130  unss1  4131  ssequn1  4132  rexun  4142  elsymdif  4204  indi  4230  undi  4231  unineq  4234  undif3  4246  rabun2  4270  reuun2  4271  undif4  4420  ssundif  4443  dfpr2  4605  elunsn  4644  elpwunsn  4645  eltpg  4647  el7g  4651  pwpr  4861  pwtp  4862  uniun  4890  iinun2  5031  iunun  5053  iunxun  5054  iinuni  5058  brun  5156  trun  5223  pwssun  5543  opthprc  5715  xpundi  5720  xpundir  5721  difxp  6154  sossfld  6177  imadifssran  6195  imadifssranOLD  6196  elsuci  6425  elsucg  6426  elsuc2g  6427  funun  6578  mptun  6677  unima  6952  eqfnun  7028  unpreima  7054  ordsucun  7825  resf1extb  7935  fnse  8134  xpord2pred  8146  xpord3pred  8153  suppofssd  8204  reldmtpos  8235  dftpos4  8246  tpostpos  8247  frrlem12  8299  frrlem13  8300  oarec  8554  brdom2  8993  unfi  9170  unxpdomlem3  9233  domunfican  9297  dfsup2  9420  wemapso2lem  9530  unwdomg  9562  unxpwdom2  9566  cantnfp1lem3  9665  rankunb  9845  djur  9981  djuunxp  9983  eldju2ndl  9986  eldju2ndr  9987  djuun  9988  iscard3  10153  kmlem2  10211  ssfin4  10369  dffin7-2  10457  fin1a2lem11  10469  fin1a2lem12  10470  cfpwsdom  10650  elgch  10688  fpwwe2lem12  10708  canthp1lem2  10719  gch2  10741  elnn0  12589  un0addcl  12620  un0mulcl  12621  elxnn0  12662  ltxr  13225  elxr  13226  xrsupexmnf  13416  xrinfmexpnf  13417  supxrun  13427  ixxun  13473  difreicc  13596  iccsplit  13597  fzsplit2  13663  elfzp1  13688  uzsplit  13710  elfzp12  13717  fzosplit  13807  fzouzsplit  13809  elfzonlteqm1  13856  elfzo0l  13871  fzosplitsni  13894  elfzr  13896  elfzlmr  13897  hashnn0pnf  14466  hashf1lem2  14581  hash2pwpr  14601  pr2pwpr  14604  ccatrn  14715  cats1un  14850  fsumsplit  15887  sumsplit  15914  fprodsplit  16113  rpnnen2lem12  16373  sumeven  16537  sumodd  16538  saddisjlem  16614  lcmfunsnlem1  16792  lcmfunsnlem2lem1  16793  lcmfunsnlem2lem2  16794  lcmfunsnlem2  16795  coprmprod  16816  coprmproddvdslem  16817  nnnn0modprm0  16964  prm23lt5  16972  vdwapun  17132  ramubcl  17176  basprssdmsets  17379  mreexmrid  17797  lubun  18669  chnccats1  18779  smndex1basss  19084  smndex1mgm  19086  smndex1mndlem  19088  smndex1n0mnd  19091  symgextf1  19615  gsumzsplit  20121  gsumzunsnd  20150  gsumunsnfd  20151  dprddisj2  20235  dmdprdsplit2lem  20241  dmdprdsplit2  20242  dprdsplit  20244  cnfldfun  21672  mplcoe1  22326  mplcoe5  22329  evlslem4  22365  mdetunilem9  22915  maducoeval2  22935  madugsum  22938  clslp  23446  islpi  23447  restntr  23480  pnfnei  23518  mnfnei  23519  iunconn  23726  refun0  23814  xkoptsub  23953  ptunhmeo  24107  fbun  24139  filconn  24182  fixufil  24221  ufildr  24230  alexsubALTlem2  24347  alexsubALTlem3  24348  alexsubALTlem4  24349  tsmssplit  24451  xrtgioo  25106  reconnlem2  25127  iccpnfcnv  25245  iccpnfhmeo  25246  rrxcph  25693  rrxdstprj1  25710  mbfss  25947  mbfmax  25950  itg2splitlem  26049  itg2split  26050  iblss2  26106  itgsplit  26136  limcdif  26176  ellimc2  26177  limcmpt  26183  limcres  26186  limccnp  26191  limccnp2  26192  limcco  26193  rollelem  26289  dvivthlem1  26308  dvne0  26311  lhop  26316  degltlem1  26370  ply1rem  26464  fta1glem2  26467  plypf1  26511  plyaddlem1  26512  plymullem1  26513  plycj  26576  plycjOLD  26578  ofmulrt  26582  taylfval  26668  abelthlem2  26741  abelthlem3  26742  reasinsin  27206  scvxcvx  27295  ppinprm  27461  chtnprm  27463  dchrfi  27564  lgsdir2  27639  2lgslem3  27713  2lgsoddprmlem3  27723  nosepdmlem  28022  sltsun1  28156  sltsun2  28157  addsproplem2  28338  addsuniflem  28369  negsid  28409  mulsproplem9  28492  sltmuls1  28515  sltmuls2  28516  precsexlem9  28583  precsexlem11  28585  ltonold  28629  usgrexmplef  29822  cffldtocusgr  30010  vtxdun  30044  eucrct2eupth  30828  shunssi  31952  atomli  32966  atoml2i  32967  rmoun  33072  rmounid  33073  nelun  33091  suppovss  33256  isoun  33277  fzsplit3  33367  eliccioo  33479  gsumwun  33619  cycpmco2  33676  cyc3co2  33683  cycpmrn  33686  elrgspnlem2  33786  ply1dg3rt0irred  34098  lindsun  34239  lbsdiflsp0  34240  ordtconnlem1  34538  xrge0iifcnv  34547  xrge0iifiso  34549  xrge0iifhom  34551  esumsplit  34667  esumpad2  34670  measvuni  34829  sxbrsigalem0  34886  bnj1138  35402  bnj1137  35608  subfacp1lem4  35917  subfacp1lem5  35918  kur14lem7  35946  satfvsucsuc  36099  satfrnmapom  36104  satf0op  36111  satf0n0  36112  sat1el2xp  36113  fmlafvel  36119  isfmlasuc  36122  fmlaomn0  36124  satfv1fvfmla1  36157  2goelgoanfmla1  36158  mrsubcv  36244  mclsax  36303  brcup  36671  refssfne  37116  ttciunun  37269  bj-eltag  37860  bj-0eltag  37861  bj-sngltag  37866  bj-projun  37877  bj-axbun  37919  bj-axadj  37924  bj-imdirco  38079  tan2h  38503  poimirlem2  38508  poimirlem8  38514  poimirlem18  38524  poimirlem21  38527  poimirlem22  38528  poimirlem23  38529  poimirlem24  38530  poimirlem25  38531  poimirlem27  38533  poimirlem29  38535  poimirlem31  38537  poimirlem32  38538  ftc1anclem1  38579  ftc1anclem5  38583  dvasin  38590  dvacos  38591  smprngopr  38954  dfsucmap3  39363  elpadd  40824  paddval0  40835  hdmaplem4  42799  mapdh9a  42814  unitscyglem2  43214  ofun  43257  lzunuz  43732  jm2.23  43956  unxpwdom3  44055  hbtlem5  44088  fzunt  44414  fzuntd  44415  fzunt1d  44416  fzuntgd  44417  rp-fakeinunass  44474  sqrtcvallem1  44590  frege133d  44724  frege83  44905  frege131  44953  frege133  44955  uneqsn  44984  clsk1indlem3  45002  ntrneixb  45054  ntrneix3  45056  ntrneix13  45058  radcnvrat  45257  bccbc  45288  undif3VD  45823  iunconnlem2  45876  permaxinf2lem  45954  fnchoice  45989  limciccioolb  46577  limcicciooub  46591  icccncfext  46841  cncfiooicclem1  46847  fourierdlem70  47130  fourierdlem80  47140  fourierdlem93  47153  fourierdlem101  47161  sge0split  47363  wrddun2  47844  chndun2  47849  chnrun2  47854  el1fzopredsuc  48340  iccpartltu  48451  iccpartgtl  48452  iccpartgt  48453  iccpartleu  48454  iccpartgel  48455  fmtno4prmfac  48601  31prm  48626  sbgoldbo  48829  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  wtgoldbnnsum4prm  48844  bgoldbnnsum3prm  48846  bgoldbtbndlem3  48849  bgoldbtbnd  48851  elclnbgrelnbgr  48867  clnbgrel  48870  clnbupgrel  48876  dfclnbgr6  48898  isubgr3stgrlem4  49011  usgrexmpl1tri  49067  usgrexmpl2nb0  49073  usgrexmpl2nb1  49074  usgrexmpl2nb2  49075  usgrexmpl2nb3  49076  usgrexmpl2nb4  49077  usgrexmpl2nb5  49078  usgrexmpl2trifr  49079  gpgprismgr4cycllem3  49139  gpgprismgr4cycllem7  49143  gpgprismgr4cycllem10  49146  smprngprmrng  49380