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

Theorem eleq2 2465
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 2398 . . . . . 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 1770 . . . 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 1633 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  <->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2400 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2400 . 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 1546   E.wex 1547    = wceq 1649    e. wcel 1721
This theorem is referenced by:  eleq12  2466  eleq2i  2468  eleq2d  2471  nelneq2  2503  dvelimdc  2560  nelne1  2656  neleq2  2661  raleqf  2860  rexeqf  2861  reueq1f  2862  rmoeq1f  2863  rabeqf  2909  clel3g  3033  clel4  3035  sbcel2gv  3181  sbnfc2  3269  difeq2  3419  uneq1  3454  ineq1  3495  unineq  3551  n0i  3593  disjel  3634  elif  3733  exsnrex  3808  sneqr  3926  preqr1  3932  preq12b  3934  prel12  3935  elunii  3980  eluniab  3987  ssuni  3997  elinti  4019  elintab  4021  intss1  4025  intmin  4030  intab  4040  iineq2  4070  dfiin2g  4084  breq  4174  zfrepclf  4286  axsep2  4291  zfauscl  4292  inuni  4322  elALT  4367  rext  4372  intid  4381  opth1  4394  opthwiener  4418  ordtri1  4574  ordtri3  4577  nsuceq0  4621  suctr  4624  ordnbtwn  4631  snnex  4672  uniuni  4675  iunpw  4718  oneqmin  4744  onuninsuci  4779  nlimsucg  4781  limomss  4809  nnlim  4817  peano5  4827  xpeq1  4851  xpeq2  4852  opthprc  4884  funopg  5444  dffv2  5755  dffo4  5844  elunirnALT  5959  f1oiso  6030  mpt2eq123  6092  ndmovg  6189  unielxp  6344  cnvf1o  6404  canth  6498  eusvobj2  6541  smoel  6581  smo11  6585  tz7.44-2  6624  oawordeulem  6756  oaordex  6760  omordi  6768  oneo  6783  oeordi  6789  oeoa  6799  oeoe  6801  nnmordi  6833  nnaordex  6840  omabs  6849  nnneo  6853  omsmolem  6855  elqsn0  6932  qsel  6942  mapsn  7014  undifixp  7057  boxriin  7063  boxcutc  7064  fineqvlem  7282  fineqv  7283  pssnn  7286  fissuni  7369  dffi2  7386  inficl  7388  dffi3  7394  wofib  7470  zfregcl  7518  suc11reg  7530  inf0  7532  inf3lem2  7540  inf3lem3  7541  infeq5i  7547  axinf2  7551  dfom3  7558  elom3  7559  noinfepOLD  7571  cantnfle  7582  oemapvali  7596  cantnflem1c  7599  cantnflem1  7601  en3lplem1  7626  en3lp  7628  tc2  7637  r1sdom  7656  rankwflemb  7675  rankval3b  7708  rankunb  7732  rankuni2b  7735  tcrank  7764  cardlim  7815  cardprclem  7822  infxpenlem  7851  alephnbtwn  7908  alephordi  7911  cardaleph  7926  alephfp  7945  alephval3  7947  aceq1  7954  aceq2  7956  dfac3  7958  dfac5lem2  7961  dfac5lem4  7963  dfac2  7967  kmlem2  7987  kmlem4  7989  coflim  8097  cfsmolem  8106  fin23lem30  8178  isf32lem2  8190  isf34lem4  8213  axdc2lem  8284  axdc3lem2  8287  axdc3lem4  8289  axdc4lem  8291  zorn2lem7  8338  axdclem  8355  brdom7disj  8365  brdom6disj  8366  axpowndlem3  8430  winainflem  8524  iswun  8535  eltskg  8581  inar1  8606  elgrug  8623  inaprc  8667  eltskm  8674  addnidpi  8734  indpi  8740  nqereu  8762  elnp  8820  elnpi  8821  genpnnp  8838  ltaddpr  8867  dfnn2  9969  dfnn3  9970  dfuzi  10316  uz11  10464  om2uzlti  11245  axdc4uz  11277  hashbclem  11656  hashf1lem2  11660  rpnnen2lem1  12769  rpnnen2lem2  12770  sadcp1  12922  ismre  13770  isacs  13831  mreclat  14568  issubm  14703  cycsubg  14923  isnsg  14924  subgacs  14930  nsgacs  14931  resghm  14977  ghmeql  14983  gsumzsplit  15484  pgpfac1lem1  15587  pgpfac1lem5  15592  pgpfac1  15593  issubrg  15823  islss  15966  lssacs  15998  lspsneq0  16043  lmhmeql  16086  lspdisjb  16153  lidl1el  16244  lidldvgen  16281  mplcoe1  16483  mplcoe2  16485  istopg  16923  fiinbas  16972  topbas  16992  ppttop  17026  pptbas  17027  epttop  17028  elcls  17092  clsndisj  17094  elcls3  17102  iscldtop  17114  neiptopnei  17151  restbas  17176  restntr  17200  pnfnei  17238  mnfnei  17239  cnpimaex  17274  lmcvg  17280  iscnp4  17281  cncnpi  17296  cnconst2  17301  cnprest  17307  cnprest2  17308  cnpdis  17311  lmss  17316  lmff  17319  cnt0  17364  ist1-3  17367  cnhaus  17372  isreg2  17395  dishaus  17400  ordthauslem  17401  cmpsublem  17416  cmpsub  17417  cmpcld  17419  hauscmplem  17423  uncon  17445  concompid  17447  concompcon  17448  concompss  17449  1stcfb  17461  1stcrest  17469  2ndcctbss  17471  2ndcomap  17474  dis2ndc  17476  1stcelcls  17477  llyeq  17486  nllyeq  17487  restnlly  17498  restlly  17499  islly2  17500  lly1stc  17512  dislly  17513  hauspwdom  17517  llycmpkgen2  17535  txbas  17552  eltx  17553  ptpjopn  17597  ptclsg  17600  dfac14lem  17602  txcnp  17605  ptcnplem  17606  ptcnp  17607  txlly  17621  pthaus  17623  txtube  17625  txhaus  17632  txlm  17633  tx1stc  17635  txkgen  17637  xkohaus  17638  xkopt  17640  xkococnlem  17644  tgqtop  17697  kqfvima  17715  kqt0lem  17721  isr0  17722  r0cld  17723  regr1lem  17724  kqreglem1  17726  kqreglem2  17727  reghmph  17778  fbssfi  17822  isfil  17832  filuni  17870  isufil  17888  isufil2  17893  uffix  17906  fixufil  17907  uffixfr  17908  uffixsn  17910  rnelfm  17938  flimopn  17960  flimrest  17968  flimcls  17970  flftg  17981  txflf  17991  fclsopni  18000  fclsrest  18009  fclscf  18010  fcfnei  18020  alexsublem  18028  alexsubALTlem3  18033  alexsubALT  18035  tmdgsum2  18079  symgtgp  18084  subgntr  18089  opnsubg  18090  tgpconcompeqg  18094  ghmcnp  18097  tgpt0  18101  divstgpopn  18102  tsmsi  18116  tsmssubm  18125  tsmssplit  18134  isust  18186  ustn0  18203  blssps  18407  blss  18408  blssexps  18409  blssex  18410  neibl  18484  blcld  18488  metss  18491  methaus  18503  met1stc  18504  met2ndci  18505  metrest  18507  prdsxmslem2  18512  metcnp3  18523  dscopn  18574  idnghm  18730  qdensere  18757  tgioo  18780  tgqioo  18784  zdis  18800  xrge0tsms  18818  cnheibor  18933  lmmbr  19164  bcthlem4  19233  ovolicc2lem5  19370  dyadmbllem  19444  i1fd  19526  itg11  19536  itg2gt0  19605  itgeq1f  19616  bddmulibl  19683  ellimc2  19717  limcnlp  19718  ellimc3  19719  limcflf  19721  limciun  19734  lhop1lem  19850  ig1pdvds  20052  plycpn  20159  aannenlem2  20199  efopn  20502  xrlimcnp  20760  wilthlem2  20805  wilthlem3  20806  wilth  20807  usgra2edg  21355  usgraedg4  21359  nbgraf1olem1  21404  nbgraf1olem3  21406  nb3graprlem1  21413  nb3graprlem2  21414  uvtx01vtx  21454  uvtxnbgravtx  21457  2trllemF  21502  wlkntrl  21515  constr1trl  21541  vdgr1a  21630  vdusgra0nedg  21632  usgravd0nedg  21636  eupath2lem1  21652  lpni  21720  rngoueqz  21971  issh  22663  pjoc1  22889  h1dn0  23007  spansneleqi  23024  nonbooli  23106  pjch  23149  pjnel  23181  cdjreui  23888  rexunirn  23931  xrge0tsmsd  24176  tpr2rico  24263  lmxrge0  24290  indval  24364  issiga  24447  isrnsigaOLD  24448  isrnsiga  24449  ismbfm  24555  isanmbfm  24559  dya2icoseg  24580  dya2iocnrect  24584  ballotlem7  24746  erdszelem1  24830  kur14lem9  24853  cnllyscon  24885  cvmcov  24903  cvmsss2  24914  cvmcov2  24915  cvmseu  24916  cvmsiota  24917  cvmopnlem  24918  cvmliftlem15  24938  rtrclreclem.trans  25099  untelirr  25110  untsucf  25112  prodeq1f  25187  dfon2lem4  25356  dfon2lem7  25359  dfon2lem9  25361  soseq  25468  frrlem4  25498  frrlem5e  25503  frrlem11  25507  nodenselem8  25556  nocvxminlem  25558  nofulllem5  25574  dfiota3  25676  funpartlem  25695  funpartfun  25696  tfrqfree  25704  linethru  25991  hilbert1.1  25992  hilbert1.2  25993  rankelg  26013  elhf2  26020  mblfinlem  26143  fneint  26247  finlocfin  26269  locfindis  26275  comppfsc  26277  neibastop2lem  26279  cover2  26305  isbnd2  26382  prdstotbnd  26393  heibor1lem  26408  grpokerinj  26450  isidl  26514  1idl  26526  0rngo  26527  ispridl  26534  smprngopr  26552  isfldidl  26568  isdmn3  26574  elmzpcl  26673  diophren  26764  dford3lem2  26988  ttac  26997  pw2f1ocnv  26998  wepwsolem  27006  kelac1  27029  f1otrspeq  27258  pmtrval  27262  sdrgacs  27377  expgrowthi  27418  dvconstbi  27419  elunif  27554  fnchoice  27567  stoweidlem27  27643  stoweidlem35  27651  stoweidlem46  27662  stoweidlem52  27668  funressnfv  27859  fnbrafvb  27885  afvco2  27907  ndmaovg  27915  aovmpt4g  27932  vdn0frgrav2  28128  vdgn0frgrav2  28129  frgrancvvdeqlem4  28136  frgrancvvdeqlem7  28139  frgrancvvdeqlemA  28140  frgrancvvdeqlemC  28142  frgrawopreg1  28153  frgrawopreg2  28154  tratrb  28331  suctrALT2VD  28657  suctrALT2  28658  en3lplem1VD  28664  en3lpVD  28666  tratrbVD  28682  suctrALTcf  28743  suctrALTcfVD  28744  suctrALT3  28745  unisnALT  28747  bnj145  28800  bnj216  28805  bnj563  28817  bnj956  28853  bnj545  28972  bnj548  28974  bnj570  28982  bnj900  29006  bnj929  29013  bnj964  29020  bnj983  29028  bnj1001  29035  bnj1145  29068  bnj1398  29109  bnj1498  29136  lsateln0  29478  ispsubsp  30227  linepsubN  30234  elpcliN  30375  dvh3dim3N  31932  dochsnnz  31933  mapdindp3  32205
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator