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

Theorem eleq2 2357
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 2290 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 186 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1806 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43anbi2d 684 . . 3  |-  ( A  =  B  ->  (
( x  =  C  /\  x  e.  A
)  <->  ( x  =  C  /\  x  e.  B ) ) )
54exbidv 1616 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  <->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2292 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2292 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73bitr4g 279 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1530   E.wex 1531    = wceq 1632    e. wcel 1696
This theorem is referenced by:  eleq12  2358  eleq2i  2360  eleq2d  2363  nelneq2  2395  dvelimdc  2452  nelne1  2548  neleq2  2551  raleqf  2745  rexeqf  2746  reueq1f  2747  rmoeq1f  2748  rabeqf  2794  clel3g  2918  clel4  2920  sbcel2gv  3064  sbnfc2  3154  difeq2  3301  uneq1  3335  ineq1  3376  unineq  3432  n0i  3473  disjel  3514  elif  3612  sneqr  3796  preqr1  3802  preq12b  3804  prel12  3805  elunii  3848  eluniab  3855  ssuni  3865  elinti  3887  elintab  3889  intss1  3893  intmin  3898  intab  3908  iineq2  3938  dfiin2g  3952  breq  4041  axrep1  4148  zfrepclf  4153  axsep2  4158  zfauscl  4159  inuni  4189  elALT  4234  rext  4238  intid  4247  opth1  4260  opthwiener  4284  ordtri1  4441  ordtri3  4444  nsuceq0  4488  suctr  4491  trsuc2OLD  4493  ordnbtwn  4499  snnex  4540  uniuni  4543  iunpw  4586  oneqmin  4612  onuninsuci  4647  nlimsucg  4649  limomss  4677  nnlim  4685  peano5  4695  xpeq1  4719  xpeq2  4720  opthprc  4752  funopg  5302  dffv2  5608  dffo4  5692  elunirnALT  5795  f1oiso  5864  mpt2eq123  5923  ndmovg  6019  unielxp  6174  cnvf1o  6233  canth  6310  eusvobj2  6353  smoel  6393  smo11  6397  tz7.44-2  6436  oawordeulem  6568  oaordex  6572  omordi  6580  oneo  6595  oeordi  6601  oeoa  6611  oeoe  6613  nnmordi  6645  nnaordex  6652  omabs  6661  nnneo  6665  omsmolem  6667  elqsn0  6744  qsel  6754  mapsn  6825  undifixp  6868  boxriin  6874  boxcutc  6875  fineqvlem  7093  fineqv  7094  pssnn  7097  fissuni  7176  dffi2  7192  inficl  7194  dffi3  7200  wofib  7276  zfregcl  7324  suc11reg  7336  inf0  7338  inf3lem2  7346  inf3lem3  7347  infeq5i  7353  axinf2  7357  dfom3  7364  elom3  7365  noinfepOLD  7377  cantnfle  7388  oemapvali  7402  cantnflem1c  7405  cantnflem1  7407  en3lplem1  7432  en3lp  7434  tc2  7443  r1sdom  7462  rankwflemb  7481  rankval3b  7514  rankunb  7538  rankuni2b  7541  tcrank  7570  cardlim  7621  cardprclem  7628  infxpenlem  7657  alephnbtwn  7714  alephordi  7717  cardaleph  7732  alephfp  7751  alephval3  7753  aceq1  7760  aceq2  7762  dfac3  7764  dfac5lem2  7767  dfac5lem4  7769  dfac2  7773  kmlem2  7793  kmlem4  7795  coflim  7903  cfsmolem  7912  fin23lem30  7984  isf32lem2  7996  isf34lem4  8019  axdc2lem  8090  axdc3lem2  8093  axdc3lem4  8095  axdc4lem  8097  zorn2lem7  8145  axdclem  8162  brdom7disj  8172  brdom6disj  8173  axpowndlem3  8237  winainflem  8331  iswun  8342  eltskg  8388  inar1  8413  elgrug  8430  inaprc  8474  eltskm  8481  addnidpi  8541  indpi  8547  nqereu  8569  elnp  8627  elnpi  8628  genpnnp  8645  ltaddpr  8674  dfnn2  9775  dfnn3  9776  dfuzi  10118  uz11  10266  om2uzlti  11029  axdc4uz  11061  hashbclem  11406  hashf1lem2  11410  rpnnen2lem1  12509  rpnnen2lem2  12510  sadcp1  12662  ismre  13508  isacs  13569  mreclat  14306  issubm  14441  cycsubg  14661  isnsg  14662  subgacs  14668  nsgacs  14669  resghm  14715  ghmeql  14721  gsumzsplit  15222  pgpfac1lem1  15325  pgpfac1lem5  15330  pgpfac1  15331  issubrg  15561  islss  15708  lssacs  15740  lspsneq0  15785  lmhmeql  15828  lspdisjb  15895  lidl1el  15986  lidldvgen  16023  mplcoe1  16225  mplcoe2  16227  istopg  16657  fiinbas  16706  topbas  16726  ppttop  16760  pptbas  16761  epttop  16762  elcls  16826  clsndisj  16828  elcls3  16836  iscldtop  16848  restbas  16905  restntr  16928  pnfnei  16966  mnfnei  16967  cnpimaex  17002  lmcvg  17008  cncnpi  17023  cnconst2  17027  cnprest  17033  cnprest2  17034  cnpdis  17037  lmss  17042  lmff  17045  cnt0  17090  ist1-3  17093  cnhaus  17098  isreg2  17121  dishaus  17126  ordthauslem  17127  cmpsublem  17142  cmpsub  17143  cmpcld  17145  hauscmplem  17149  uncon  17171  concompid  17173  concompcon  17174  concompss  17175  1stcfb  17187  1stcrest  17195  2ndcctbss  17197  2ndcomap  17200  dis2ndc  17202  1stcelcls  17203  llyeq  17212  nllyeq  17213  restnlly  17224  restlly  17225  islly2  17226  lly1stc  17238  dislly  17239  hauspwdom  17243  llycmpkgen2  17261  txbas  17278  eltx  17279  ptpjopn  17322  ptclsg  17325  dfac14lem  17327  txcnp  17330  ptcnplem  17331  ptcnp  17332  txlly  17346  pthaus  17348  txtube  17350  txhaus  17357  txlm  17358  tx1stc  17360  txkgen  17362  xkohaus  17363  xkopt  17365  xkococnlem  17369  tgqtop  17419  kqfvima  17437  kqt0lem  17443  isr0  17444  r0cld  17445  regr1lem  17446  kqreglem1  17448  kqreglem2  17449  reghmph  17500  fbssfi  17548  isfil  17558  filuni  17596  isufil  17614  isufil2  17619  uffix  17632  fixufil  17633  uffixfr  17634  uffixsn  17636  rnelfm  17664  flimopn  17686  flimrest  17694  flimcls  17696  flftg  17707  txflf  17717  fclsopni  17726  fclsrest  17735  fclscf  17736  fcfnei  17746  alexsublem  17754  alexsubALTlem3  17759  alexsubALT  17761  tmdgsum2  17795  symgtgp  17800  subgntr  17805  opnsubg  17806  tgpconcompeqg  17810  ghmcnp  17813  tgpt0  17817  divstgpopn  17818  tsmsi  17832  tsmssubm  17841  tsmssplit  17850  blss  17988  blssex  17989  neibl  18063  blcld  18067  metss  18070  methaus  18082  met1stc  18083  met2ndci  18084  metrest  18086  prdsxmslem2  18091  metcnp3  18102  dscopn  18112  idnghm  18268  qdensere  18295  tgioo  18318  tgqioo  18322  zdis  18338  xrge0tsms  18355  cnheibor  18469  lmmbr  18700  bcthlem4  18765  ovolicc2lem5  18896  dyadmbllem  18970  i1fd  19052  itg11  19062  itg2gt0  19131  itgeq1f  19142  bddmulibl  19209  ellimc2  19243  limcnlp  19244  ellimc3  19245  limcflf  19247  limciun  19260  lhop1lem  19376  ig1pdvds  19578  plycpn  19685  aannenlem2  19725  efopn  20021  xrlimcnp  20279  wilthlem2  20323  wilthlem3  20324  wilth  20325  lpni  20862  rngoueqz  21113  issh  21803  pjoc1  22029  h1dn0  22147  spansneleqi  22164  nonbooli  22246  pjch  22289  pjnel  22321  cdjreui  23028  ballotlem7  23110  rexunirn  23156  abfmpunirn  23231  abfmpeld  23233  abfmpel  23234  tpr2rico  23311  lmxrge0  23390  xrge0tsmsd  23397  issiga  23487  isrnsigaOLD  23488  isrnsiga  23489  ismbfm  23572  isanmbfm  23576  dya2iocseg  23594  indval  23612  erdszelem1  23737  kur14lem9  23760  cnllyscon  23791  cvmcov  23809  cvmsss2  23820  cvmcov2  23821  cvmseu  23822  cvmsiota  23823  cvmopnlem  23824  cvmliftlem15  23844  vdgr1a  23912  eupath2lem1  23916  rtrclreclem.trans  24058  untelirr  24069  untsucf  24071  cprodeq1f  24130  dfon2lem4  24213  dfon2lem7  24216  dfon2lem9  24218  soseq  24325  frrlem4  24355  frrlem5e  24360  frrlem11  24364  nodenselem8  24413  nocvxminlem  24415  nofulllem5  24431  dfiota3  24533  funpartlem  24552  funpartfun  24553  tfrqfree  24561  linethru  24848  hilbert1.1  24849  hilbert1.2  24850  rankelg  24870  elhf2  24877  cbicp  25269  prl2  25272  preoref22  25332  defse3  25375  prodeq3ii  25411  isidlNEW  25549  glmrngo  25585  elioo1t3  25605  nsn  25633  iscnp4  25666  prdnei  25676  bwt2  25695  altretop  25703  tcnvec  25793  elcarelcl  26009  prismorcset  26017  morcatset1  26018  isgraphmrph2  26027  domcatfun  26028  domcatsetval2  26032  domcatval2  26034  codcatfun  26037  codcatval2  26040  prismorcset3  26041  rocatval2  26063  setiscat  26082  indcls2  26099  clscnc  26113  pfsubkl  26150  elhaltdp2  26171  tethpnc2  26174  lineval42  26183  lineval22  26185  isibg2  26213  isibcg  26294  fneint  26380  finlocfin  26402  locfindis  26408  comppfsc  26410  neibastop2lem  26412  cover2  26461  isbnd2  26610  prdstotbnd  26621  heibor1lem  26636  grpokerinj  26678  isidl  26742  1idl  26754  0rngo  26755  ispridl  26762  smprngopr  26780  isfldidl  26796  isdmn3  26802  elmzpcl  26907  diophren  26999  dford3lem2  27223  ttac  27232  pw2f1ocnv  27233  wepwsolem  27241  kelac1  27264  f1otrspeq  27493  pmtrval  27497  sdrgacs  27612  expgrowthi  27653  dvconstbi  27654  elunif  27790  fnchoice  27803  stoweidlem27  27879  stoweidlem35  27887  stoweidlem46  27898  stoweidlem48  27900  stoweidlem52  27904  stoweidlem59  27911  funressnfv  28096  fnbrafvb  28122  afvco2  28144  ndmaovg  28152  aovmpt4g  28169  nb3graprlem1  28287  nb3graprlem2  28288  uvtx01vtx  28305  uvtxnbgravtx  28308  tratrb  28598  suctrALT2VD  28928  suctrALT2  28929  en3lplem1VD  28935  en3lpVD  28937  tratrbVD  28953  suctrALTcf  29014  suctrALTcfVD  29015  suctrALT3  29016  unisnALT  29018  suctrALT4  29020  bnj145  29071  bnj216  29076  bnj563  29088  bnj956  29124  bnj545  29243  bnj548  29245  bnj570  29253  bnj900  29277  bnj929  29284  bnj964  29291  bnj983  29299  bnj1001  29306  bnj1145  29339  bnj1398  29380  bnj1498  29407  lsateln0  29807  ispsubsp  30556  linepsubN  30563  elpcliN  30704  dvh3dim3N  32261  dochsnnz  32262  mapdindp3  32534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator