MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleq2 Unicode version

Theorem eleq2 2496
Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eleq2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )

Proof of Theorem eleq2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2429 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 187 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1774 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43anbi2d 685 . . 3  |-  ( A  =  B  ->  (
( x  =  C  /\  x  e.  A
)  <->  ( x  =  C  /\  x  e.  B ) ) )
54exbidv 1636 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  <->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2431 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2431 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73bitr4g 280 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549   E.wex 1550    = wceq 1652    e. wcel 1725
This theorem is referenced by:  eleq12  2497  eleq2i  2499  eleq2d  2502  nelneq2  2534  dvelimdc  2591  nelne1  2687  neleq2  2692  raleqf  2892  rexeqf  2893  reueq1f  2894  rmoeq1f  2895  rabeqf  2941  clel3g  3065  clel4  3067  sbcel2gv  3213  sbnfc2  3301  difeq2  3451  uneq1  3486  ineq1  3527  unineq  3583  n0i  3625  disjel  3666  elif  3765  exsnrex  3840  sneqr  3958  preqr1  3964  preq12b  3966  prel12  3967  elunii  4012  eluniab  4019  ssuni  4029  elinti  4051  elintab  4053  intss1  4057  intmin  4062  intab  4072  iineq2  4102  dfiin2g  4116  breq  4206  zfrepclf  4318  axsep2  4323  zfauscl  4324  inuni  4354  elALT  4399  rext  4404  intid  4413  opth1  4426  opthwiener  4450  ordtri1  4606  ordtri3  4609  nsuceq0  4653  suctr  4656  ordnbtwn  4663  snnex  4704  uniuni  4707  iunpw  4750  oneqmin  4776  onuninsuci  4811  nlimsucg  4813  limomss  4841  nnlim  4849  peano5  4859  xpeq1  4883  xpeq2  4884  opthprc  4916  funopg  5476  dffv2  5787  dffo4  5876  elunirnALT  5991  f1oiso  6062  mpt2eq123  6124  ndmovg  6221  unielxp  6376  cnvf1o  6436  canth  6530  eusvobj2  6573  smoel  6613  smo11  6617  tz7.44-2  6656  oawordeulem  6788  oaordex  6792  omordi  6800  oneo  6815  oeordi  6821  oeoa  6831  oeoe  6833  nnmordi  6865  nnaordex  6872  omabs  6881  nnneo  6885  omsmolem  6887  elqsn0  6964  qsel  6974  mapsn  7046  undifixp  7089  boxriin  7095  boxcutc  7096  fineqvlem  7314  fineqv  7315  pssnn  7318  fissuni  7402  dffi2  7419  inficl  7421  dffi3  7427  wofib  7503  zfregcl  7551  suc11reg  7563  inf0  7565  inf3lem2  7573  inf3lem3  7574  infeq5i  7580  axinf2  7584  dfom3  7591  elom3  7592  noinfepOLD  7604  cantnfle  7615  oemapvali  7629  cantnflem1c  7632  cantnflem1  7634  en3lplem1  7659  en3lp  7661  tc2  7670  r1sdom  7689  rankwflemb  7708  rankval3b  7741  rankunb  7765  rankuni2b  7768  tcrank  7797  cardlim  7848  cardprclem  7855  infxpenlem  7884  alephnbtwn  7941  alephordi  7944  cardaleph  7959  alephfp  7978  alephval3  7980  aceq1  7987  aceq2  7989  dfac3  7991  dfac5lem2  7994  dfac5lem4  7996  dfac2  8000  kmlem2  8020  kmlem4  8022  coflim  8130  cfsmolem  8139  fin23lem30  8211  isf32lem2  8223  isf34lem4  8246  axdc2lem  8317  axdc3lem2  8320  axdc3lem4  8322  axdc4lem  8324  zorn2lem7  8371  axdclem  8388  brdom7disj  8398  brdom6disj  8399  axpowndlem3  8463  winainflem  8557  iswun  8568  eltskg  8614  inar1  8639  elgrug  8656  inaprc  8700  eltskm  8707  addnidpi  8767  indpi  8773  nqereu  8795  elnp  8853  elnpi  8854  genpnnp  8871  ltaddpr  8900  dfnn2  10002  dfnn3  10003  dfuzi  10349  uz11  10497  om2uzlti  11278  axdc4uz  11310  hashbclem  11689  hashf1lem2  11693  rpnnen2lem1  12802  rpnnen2lem2  12803  sadcp1  12955  ismre  13803  isacs  13864  mreclat  14601  issubm  14736  cycsubg  14956  isnsg  14957  subgacs  14963  nsgacs  14964  resghm  15010  ghmeql  15016  gsumzsplit  15517  pgpfac1lem1  15620  pgpfac1lem5  15625  pgpfac1  15626  issubrg  15856  islss  15999  lssacs  16031  lspsneq0  16076  lmhmeql  16119  lspdisjb  16186  lidl1el  16277  lidldvgen  16314  mplcoe1  16516  mplcoe2  16518  istopg  16956  fiinbas  17005  topbas  17025  ppttop  17059  pptbas  17060  epttop  17061  elcls  17125  clsndisj  17127  elcls3  17135  iscldtop  17147  neiptopnei  17184  restbas  17210  restntr  17234  pnfnei  17272  mnfnei  17273  cnpimaex  17308  lmcvg  17314  iscnp4  17315  cncnpi  17330  cnconst2  17335  cnprest  17341  cnprest2  17342  cnpdis  17345  lmss  17350  lmff  17353  cnt0  17398  ist1-3  17401  cnhaus  17406  isreg2  17429  dishaus  17434  ordthauslem  17435  cmpsublem  17450  cmpsub  17451  cmpcld  17453  hauscmplem  17457  bwth  17461  uncon  17480  concompid  17482  concompcon  17483  concompss  17484  1stcfb  17496  1stcrest  17504  2ndcctbss  17506  2ndcomap  17509  dis2ndc  17511  1stcelcls  17512  llyeq  17521  nllyeq  17522  restnlly  17533  restlly  17534  islly2  17535  lly1stc  17547  dislly  17548  hauspwdom  17552  llycmpkgen2  17570  txbas  17587  eltx  17588  ptpjopn  17632  ptclsg  17635  dfac14lem  17637  txcnp  17640  ptcnplem  17641  ptcnp  17642  txlly  17656  pthaus  17658  txtube  17660  txhaus  17667  txlm  17668  tx1stc  17670  txkgen  17672  xkohaus  17673  xkopt  17675  xkococnlem  17679  tgqtop  17732  kqfvima  17750  kqt0lem  17756  isr0  17757  r0cld  17758  regr1lem  17759  kqreglem1  17761  kqreglem2  17762  reghmph  17813  fbssfi  17857  isfil  17867  filuni  17905  isufil  17923  isufil2  17928  uffix  17941  fixufil  17942  uffixfr  17943  uffixsn  17945  rnelfm  17973  flimopn  17995  flimrest  18003  flimcls  18005  flftg  18016  txflf  18026  fclsopni  18035  fclsrest  18044  fclscf  18045  fcfnei  18055  alexsublem  18063  alexsubALTlem3  18068  alexsubALT  18070  tmdgsum2  18114  symgtgp  18119  subgntr  18124  opnsubg  18125  tgpconcompeqg  18129  ghmcnp  18132  tgpt0  18136  divstgpopn  18137  tsmsi  18151  tsmssubm  18160  tsmssplit  18169  isust  18221  ustn0  18238  blssps  18442  blss  18443  blssexps  18444  blssex  18445  neibl  18519  blcld  18523  metss  18526  methaus  18538  met1stc  18539  met2ndci  18540  metrest  18542  prdsxmslem2  18547  metcnp3  18558  dscopn  18609  idnghm  18765  qdensere  18792  tgioo  18815  tgqioo  18819  zdis  18835  xrge0tsms  18853  cnheibor  18968  lmmbr  19199  bcthlem4  19268  ovolicc2lem5  19405  dyadmbllem  19479  i1fd  19561  itg11  19571  itg2gt0  19640  itgeq1f  19651  bddmulibl  19718  ellimc2  19752  limcnlp  19753  ellimc3  19754  limcflf  19756  limciun  19769  lhop1lem  19885  ig1pdvds  20087  plycpn  20194  aannenlem2  20234  efopn  20537  xrlimcnp  20795  wilthlem2  20840  wilthlem3  20841  wilth  20842  usgra2edg  21390  usgraedg4  21394  nbgraf1olem1  21439  nbgraf1olem3  21441  nb3graprlem1  21448  nb3graprlem2  21449  uvtx01vtx  21489  uvtxnbgravtx  21492  2trllemF  21537  wlkntrl  21550  constr1trl  21576  vdgr1a  21665  vdusgra0nedg  21667  usgravd0nedg  21671  eupath2lem1  21687  lpni  21755  rngoueqz  22006  issh  22698  pjoc1  22924  h1dn0  23042  spansneleqi  23059  nonbooli  23141  pjch  23184  pjnel  23216  cdjreui  23923  rexunirn  23966  xrge0tsmsd  24211  tpr2rico  24298  lmxrge0  24325  indval  24399  issiga  24482  isrnsigaOLD  24483  isrnsiga  24484  ismbfm  24590  isanmbfm  24594  dya2icoseg  24615  dya2iocnrect  24619  ballotlem7  24781  erdszelem1  24865  kur14lem9  24888  cnllyscon  24920  cvmcov  24938  cvmsss2  24949  cvmcov2  24950  cvmseu  24951  cvmsiota  24952  cvmopnlem  24953  cvmliftlem15  24973  rtrclreclem.trans  25134  untelirr  25145  untsucf  25147  prodeq1f  25223  dfon2lem4  25397  dfon2lem7  25400  dfon2lem9  25402  soseq  25509  frrlem4  25539  frrlem5e  25544  frrlem11  25548  nodenselem8  25597  nocvxminlem  25599  nofulllem5  25615  dfiota3  25718  funpartlem  25737  funpartfun  25738  tfrqfree  25746  linethru  26035  hilbert1.1  26036  hilbert1.2  26037  rankelg  26057  elhf2  26064  mblfinlem  26190  fneint  26294  finlocfin  26316  locfindis  26322  comppfsc  26324  neibastop2lem  26326  cover2  26352  isbnd2  26429  prdstotbnd  26440  heibor1lem  26455  grpokerinj  26497  isidl  26561  1idl  26573  0rngo  26574  ispridl  26581  smprngopr  26599  isfldidl  26615  isdmn3  26621  elmzpcl  26720  diophren  26811  dford3lem2  27035  ttac  27044  pw2f1ocnv  27045  wepwsolem  27053  kelac1  27076  f1otrspeq  27305  pmtrval  27309  sdrgacs  27424  expgrowthi  27465  dvconstbi  27466  elunif  27601  fnchoice  27614  stoweidlem27  27690  stoweidlem35  27698  stoweidlem46  27709  stoweidlem52  27715  funressnfv  27906  fnbrafvb  27932  afvco2  27954  ndmaovg  27962  aovmpt4g  27979  lswrd0  28150  vdn0frgrav2  28272  vdgn0frgrav2  28273  frgrancvvdeqlem4  28280  frgrancvvdeqlem7  28283  frgrancvvdeqlemA  28284  frgrancvvdeqlemC  28286  frgrawopreg1  28297  frgrawopreg2  28298  tratrb  28475  suctrALT2VD  28802  suctrALT2  28803  en3lplem1VD  28809  en3lpVD  28811  tratrbVD  28827  suctrALTcf  28888  suctrALTcfVD  28889  suctrALT3  28890  unisnALT  28892  bnj145  28948  bnj216  28953  bnj563  28965  bnj956  29001  bnj545  29120  bnj548  29122  bnj570  29130  bnj900  29154  bnj929  29161  bnj964  29168  bnj983  29176  bnj1001  29183  bnj1145  29216  bnj1398  29257  bnj1498  29284  lsateln0  29632  ispsubsp  30381  linepsubN  30388  elpcliN  30529  dvh3dim3N  32086  dochsnnz  32087  mapdindp3  32359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-clel 2431
  Copyright terms: Public domain W3C validator