Theorem elun 4104

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908

This theorem is referenced by:  elunnel1  4105  elunnel2  4106  uneqri  4107  uncom  4109  uneq1  4112  nfun  4121  unass  4123  ssun1  4129  elunant  4135  unss1  4136  ssequn1  4137  rexun  4147  elsymdif  4209  indi  4235  undi  4236  unineq  4239  undif3  4251  rabun2  4275  reuun2  4276  undif4  4418  ssundif  4439  dfpr2  4598  elunsn  4635  elpwunsn  4636  eltpg  4638  el7g  4642  pwpr  4852  pwtp  4853  uniun  4881  iinun2  5022  iunun  5042  iunxun  5043  iinuni  5047  brun  5143  pwssun  5511  opthprc  5683  xpundi  5688  xpundir  5689  imadifssran  6100  difxp  6113  sossfld  6135  elsuci  6376  elsucg  6377  elsuc2g  6378  funun  6528  mptun  6628  unima  6898  eqfnun  6971  unpreima  6997  ordsucun  7758  resf1extb  7867  fnse  8066  xpord2pred  8078  xpord3pred  8085  suppofssd  8136  reldmtpos  8167  dftpos4  8178  tpostpos  8179  frrlem12  8230  frrlem13  8231  oarec  8480  brdom2  8907  unfi  9085  unxpdomlem3  9147  domunfican  9211  dfsup2  9334  wemapso2lem  9444  unwdomg  9476  unxpwdom2  9480  cantnfp1lem3  9576  rankunb  9746  djur  9815  djuunxp  9817  eldju2ndl  9820  eldju2ndr  9821  djuun  9822  iscard3  9987  kmlem2  10046  ssfin4  10204  dffin7-2  10292  fin1a2lem11  10304  fin1a2lem12  10305  cfpwsdom  10478  elgch  10516  fpwwe2lem12  10536  canthp1lem2  10547  gch2  10569  elnn0  12386  un0addcl  12417  un0mulcl  12418  elxnn0  12459  ltxr  13017  elxr  13018  xrsupexmnf  13207  xrinfmexpnf  13208  supxrun  13218  ixxun  13264  difreicc  13387  iccsplit  13388  fzsplit2  13452  elfzp1  13477  uzsplit  13499  elfzp12  13506  fzosplit  13595  fzouzsplit  13597  elfzonlteqm1  13644  elfzo0l  13659  fzosplitsni  13681  elfzr  13683  elfzlmr  13684  hashnn0pnf  14249  hashf1lem2  14363  hash2pwpr  14383  pr2pwpr  14386  ccatrn  14496  cats1un  14627  fsumsplit  15648  sumsplit  15675  fprodsplit  15873  rpnnen2lem12  16134  sumeven  16298  sumodd  16299  saddisjlem  16375  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  coprmprod  16572  coprmproddvdslem  16573  nnnn0modprm0  16718  prm23lt5  16726  vdwapun  16886  ramubcl  16930  basprssdmsets  17132  mreexmrid  17549  lubun  18421  smndex1basss  18779  smndex1mgm  18781  smndex1mndlem  18783  smndex1n0mnd  18786  symgextf1  19300  gsumzsplit  19806  gsumzunsnd  19835  gsumunsnfd  19836  dprddisj2  19920  dmdprdsplit2lem  19926  dmdprdsplit2  19927  dprdsplit  19929  cnfldfun  21275  cnfldfunOLD  21288  mplcoe1  21942  mplcoe5  21945  evlslem4  21981  mdetunilem9  22505  maducoeval2  22525  madugsum  22528  clslp  23033  islpi  23034  restntr  23067  pnfnei  23105  mnfnei  23106  iunconn  23313  refun0  23400  xkoptsub  23539  ptunhmeo  23693  fbun  23725  filconn  23768  fixufil  23807  ufildr  23816  alexsubALTlem2  23933  alexsubALTlem3  23934  alexsubALTlem4  23935  tsmssplit  24037  xrtgioo  24693  reconnlem2  24714  iccpnfcnv  24840  iccpnfhmeo  24841  rrxcph  25290  rrxdstprj1  25307  mbfss  25545  mbfmax  25548  itg2splitlem  25647  itg2split  25648  iblss2  25705  itgsplit  25735  limcdif  25775  ellimc2  25776  limcmpt  25782  limcres  25785  limccnp  25790  limccnp2  25791  limcco  25792  rollelem  25891  dvivthlem1  25911  dvne0  25914  lhop  25919  degltlem1  25975  ply1rem  26069  fta1glem2  26072  plypf1  26115  plyaddlem1  26116  plymullem1  26117  plycj  26181  plycjOLD  26183  ofmulrt  26187  taylfval  26264  abelthlem2  26340  abelthlem3  26341  reasinsin  26804  scvxcvx  26894  ppinprm  27060  chtnprm  27062  dchrfi  27164  lgsdir2  27239  2lgslem3  27313  2lgsoddprmlem3  27323  nosepdmlem  27593  ssltun1  27719  ssltun2  27720  addsproplem2  27882  addsuniflem  27913  negsid  27952  mulsproplem9  28032  ssltmul1  28055  ssltmul2  28056  precsexlem9  28122  precsexlem11  28124  sltonold  28167  usgrexmplef  29204  cffldtocusgr  29392  cffldtocusgrOLD  29393  vtxdun  29427  eucrct2eupth  30189  shunssi  31312  atomli  32326  atoml2i  32327  rmoun  32438  rmounid  32439  nelun  32457  suppovss  32624  isoun  32645  fzsplit3  32737  eliccioo  32872  chnccats1  32958  gsumwun  33019  cycpmco2  33076  cyc3co2  33083  cycpmrn  33086  elrgspnlem2  33184  ply1dg3rt0irred  33519  lindsun  33598  lbsdiflsp0  33599  ordtconnlem1  33897  xrge0iifcnv  33906  xrge0iifiso  33908  xrge0iifhom  33910  esumsplit  34026  esumpad2  34029  measvuni  34187  sxbrsigalem0  34245  bnj1138  34761  bnj1137  34968  subfacp1lem4  35166  subfacp1lem5  35167  kur14lem7  35195  satfvsucsuc  35348  satfrnmapom  35353  satf0op  35360  satf0n0  35361  sat1el2xp  35362  fmlafvel  35368  isfmlasuc  35371  fmlaomn0  35373  satfv1fvfmla1  35406  2goelgoanfmla1  35407  mrsubcv  35493  mclsax  35552  brcup  35923  refssfne  36342  bj-eltag  36961  bj-0eltag  36962  bj-sngltag  36967  bj-projun  36978  bj-axbun  37020  bj-axadj  37025  bj-imdirco  37174  tan2h  37602  poimirlem2  37612  poimirlem8  37618  poimirlem18  37628  poimirlem21  37631  poimirlem22  37632  poimirlem23  37633  poimirlem24  37634  poimirlem25  37635  poimirlem27  37637  poimirlem29  37639  poimirlem31  37641  poimirlem32  37642  ftc1anclem1  37683  ftc1anclem5  37687  dvasin  37694  dvacos  37695  smprngopr  38042  elpadd  39788  paddval0  39799  hdmaplem4  41763  mapdh9a  41778  unitscyglem2  42179  ofun  42219  lzunuz  42751  jm2.23  42979  unxpwdom3  43078  hbtlem5  43111  fzunt  43438  fzuntd  43439  fzunt1d  43440  fzuntgd  43441  rp-fakeinunass  43498  sqrtcvallem1  43614  frege133d  43748  frege83  43929  frege131  43977  frege133  43979  uneqsn  44008  clsk1indlem3  44026  ntrneixb  44078  ntrneix3  44080  ntrneix13  44082  radcnvrat  44297  bccbc  44328  undif3VD  44865  iunconnlem2  44918  permaxinf2lem  44996  fnchoice  45017  limciccioolb  45612  limcicciooub  45628  icccncfext  45878  cncfiooicclem1  45884  fourierdlem70  46167  fourierdlem80  46177  fourierdlem93  46190  fourierdlem101  46198  sge0split  46400  el1fzopredsuc  47319  iccpartltu  47419  iccpartgtl  47420  iccpartgt  47421  iccpartleu  47422  iccpartgel  47423  fmtno4prmfac  47566  31prm  47591  sbgoldbo  47781  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  bgoldbtbndlem3  47801  bgoldbtbnd  47803  elclnbgrelnbgr  47819  clnbgrel  47822  clnbupgrel  47828  dfclnbgr6  47850  isubgr3stgrlem4  47963  usgrexmpl1tri  48019  usgrexmpl2nb0  48025  usgrexmpl2nb1  48026  usgrexmpl2nb2  48027  usgrexmpl2nb3  48028  usgrexmpl2nb4  48029  usgrexmpl2nb5  48030  usgrexmpl2trifr  48031  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem10  48098