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

Theorem eleq2i 2347
Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eleq1i.1  |-  A  =  B
Assertion
Ref Expression
eleq2i  |-  ( C  e.  A  <->  C  e.  B )

Proof of Theorem eleq2i
StepHypRef Expression
1 eleq1i.1 . 2  |-  A  =  B
2 eleq2 2344 . 2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
31, 2ax-mp 8 1  |-  ( C  e.  A  <->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    e. wcel 1684
This theorem is referenced by:  eleq12i  2348  eleqtri  2355  eleq2s  2375  hbxfreq  2386  abeq2i  2390  abeq1i  2391  nfceqi  2415  raleqbii  2573  rexeqbii  2574  rabeq2i  2785  elab2g  2916  elrabf  2922  elrab2  2925  cbvsbc  3019  elin2  3359  dfnul2  3457  noel  3459  eltpg  3676  tpid3g  3741  elunirab  3840  elintrab  3874  disjxiun  4020  exss  4236  elop  4239  brabsb  4276  brabga  4279  pofun  4330  elsuci  4458  elsucg  4459  elsuc2g  4460  suceloni  4604  elxp  4706  brab2a  4738  opeliunxp  4740  brab2ga  4763  elcnv  4858  elrnmptg  4929  opelres  4960  rninxp  5117  elfv  5523  fv01  5559  dffv2  5592  fvopab3g  5598  fvmptex  5610  f0cli  5671  fmptco  5691  funfvima  5753  elunirn  5777  fliftel  5808  eloprabga  5934  elrnmpt2  5957  ovid  5964  offval  6085  1st2val  6145  2nd2val  6146  fsplit  6223  xporderlem  6226  brtpos2  6240  fvopab5  6289  opabiota  6293  issmo  6365  smores3  6370  tfrlem7  6399  tfrlem9  6401  tfrlem9a  6402  tfr2b  6412  tfr2  6414  rdgsuc  6437  frsucmptn  6451  tz7.48-2  6454  el1o  6498  dif1o  6499  ondif2  6501  oawordeulem  6552  elecg  6698  brecop  6751  erovlem  6754  eceqoveq  6763  ovec  6768  mapsncnv  6814  mptelixpg  6853  brsdom  6884  isfi  6885  enssdom  6886  brdom2  6891  map1  6939  xpcomco  6952  brsdom2  6985  cnfcom2lem  7404  epfrs  7413  en3lplem2  7417  r1limg  7443  r1ord  7452  r1ord3  7454  tz9.12lem3  7461  rankvaln  7471  r1elss  7478  rankpwi  7495  ssrankr1  7507  r1val3  7510  r1pw  7517  rankr1b  7536  isnum2  7578  cardprclem  7612  infxpenlem  7641  alephcard  7697  alephnbtwn  7698  alephnbtwn2  7699  alephord2  7703  alephsdom  7713  dfac3  7748  dfac5lem2  7751  dfac5lem3  7752  dfac5lem5  7754  pwsdompw  7830  cfub  7875  cardcf  7878  cflecard  7879  cfle  7880  cflim2  7889  cofsmo  7895  cfidm  7901  isfin3  7922  isfin5  7925  isfin6  7926  sdom2en01  7928  fin23lem26  7951  fin23lem30  7968  isf32lem5  7983  itunitc1  8046  ituniiun  8048  axdc3lem2  8077  axdc3lem3  8078  axcclem  8083  axdclem  8146  iunfo  8161  iundom2g  8162  cardidg  8170  konigthlem  8190  alephadd  8199  alephreg  8204  pwcfsdom  8205  cfpwsdom  8206  elgch  8244  fpwwe2lem12  8263  canth4  8269  wunex2  8360  r1tskina  8404  elni  8500  nlt1pi  8530  adderpq  8580  mulerpq  8581  recmulnq  8588  opelcn  8751  opelreal  8752  elreal  8753  elreal2  8754  0ncn  8755  addcnsr  8757  mulcnsr  8758  xrlenlt  8890  elnn0  9967  elnnne0  9979  un0addcl  9997  un0mulcl  9998  uztrn2  10245  elnnuz  10264  elnn0uz  10265  elq  10318  elxr  10458  elfzm1b  10860  uzrdgfni  11021  fzennn  11030  ser0  11098  iswrd  11415  zsum  12191  sumz  12195  sumss  12197  fsumcvg3  12202  abscvgcvg  12277  isumshft  12298  ruclem6  12513  divides  12533  sadc0  12645  eulerthlem2  12850  4sqlem2  12996  4sqlem12  13003  vdwpc  13027  xpscf  13468  cidpropd  13613  oppcsect  13676  funcpropd  13774  natpropd  13850  arwhoma  13877  eldmcoa  13897  pospo  14107  psss  14323  ismnd  14369  ghmeqker  14709  cntri  14806  oppgsubg  14836  efgsfo  15048  efgrelexlemb  15059  lt6abl  15181  dmdprd  15236  dprdval  15238  dprdw  15245  isnirred  15482  isrhm  15501  issrng  15615  lspexchn2  15884  lspindp2l  15887  lspindp2  15888  lbsextlem2  15912  evlslem4  16245  ply1bascl2  16285  eltopspOLD  16656  istpsOLD  16658  istps  16674  mretopd  16829  lpdifsn  16875  restcls  16911  perfopn  16915  pnfnei  16950  mnfnei  16951  lmss  17026  hauscmplem  17133  is2ndc  17172  2ndcdisj  17182  hausnlly  17219  txuni2  17260  ptpjpre1  17266  elpt  17267  dfac14  17312  xkococn  17354  fbasrn  17579  fin1aufil  17627  elfm2  17643  elfm3  17645  fbflim  17671  flffbas  17690  cnpflf2  17695  fclsbas  17716  tsmssubm  17825  imasdsf1olem  17937  isnghm  18232  opnreen  18336  iccpnfcnv  18442  minveclem3b  18792  ovoliunlem1  18861  ioombl1lem4  18918  subopnmbl  18959  vitalilem2  18964  vitalilem3  18965  mbfimaopnlem  19010  mbfimaopn2  19012  itg2l  19084  dvply1  19664  vieta1lem1  19690  vieta1lem2  19691  elaa  19696  taylthlem2  19753  abelthlem6  19812  abelthlem9  19816  sinq34lt0t  19877  ellogrn  19917  dvrelog  19984  ellogdm  19986  logtayl2  20009  cxpcn3lem  20087  cxpcn3  20088  1cubr  20138  atandm  20172  atanf  20176  reasinsin  20192  atans2  20227  dmarea  20252  xrlimcnp  20263  amgmlem  20284  dvdsflip  20422  ppiublem1  20441  lgsdir2lem2  20563  lgsquadlem1  20593  lgsquadlem2  20594  2sqlem1  20602  rpvmasum2  20661  issmgrp  21001  ismndo  21010  isrngo  21045  isdivrngo  21098  isvclem  21133  isnvlem  21166  vsfval  21191  h2hlm  21560  hhcmpl  21779  hhcms  21782  elch0  21833  omlsilem  21981  h1de2ctlem  22134  elspansni  22137  nonbooli  22230  spansncvi  22231  mayete3iOLD  22308  adjeq  22515  cnlnssadj  22660  cnvbraval  22690  ballotlem2  23047  ballotlemfmpn  23053  ballotlem7  23094  ballotth  23096  elxrge02  23116  ssiun3  23156  cntnevol  23175  fmptcof2  23229  fzssnn  23276  xrge0iifcnv  23315  xrge0iifiso  23317  xrge0iifhom  23319  pnfneige0  23374  gsumpropd2lem  23379  logblt  23408  esumnul  23427  measbase  23528  measvuni  23542  ismbfm  23557  elmbfmvol2  23572  isrrvv  23646  coinfliprv  23683  subfacp1lem5  23715  ghomgrpilem2  23993  elrn3  24120  dfon2lem7  24145  eltrpred  24229  wfrlem5  24260  wfrlem9  24264  wfrlem11  24266  wfrlem12  24267  wfr2  24273  frrlem5  24285  frrlem5e  24289  frrlem11  24293  nofulllem5  24360  elsymdif  24367  brsset  24429  eltrans  24431  elfix  24443  ellimits  24450  elfuns  24454  elsingles  24457  eleenn  24524  fvtransport  24655  brcolinear2  24681  fvray  24764  linedegen  24766  fvline  24767  ellines  24775  bpolydiflem  24789  bpoly2  24792  bpoly3  24793  bpoly4  24794  elhf  24804  hfninf  24816  prmapcp2  25157  isoriso  25212  supaub  25273  supwlub  25274  geme2  25275  isdir2  25292  cbvprodi  25312  zintdom  25438  vecval1b  25451  vecval3b  25452  muldisc  25481  osneisi  25531  islimrs  25580  islimrs3  25581  islimrs4  25582  ismgra  25710  isalg  25721  algi  25727  isded  25736  dedi  25737  rdmob  25748  dmrngcmp  25751  iscatOLD  25754  cati  25755  idmon  25817  cinvlem3  25830  idsubidsup  25857  idsubfun  25858  propsrc  25868  isntr  25873  islimcat  25876  cmp2morpcats  25961  cmp2morpdom  25964  cmpidmor2  25969  clscnc  26010  bisig0  26062  isibcg  26191  fnessref  26293  sdclem2  26452  sdclem1  26453  fdc  26455  caushft  26477  pellex  26920  rmspecnonsq  26992  islmodfg  27167  dsmmelbas  27205  lindsind2  27289  islindf4  27308  aaitgo  27367  pmtrfrn  27400  matrcl  27466  climsuselem1  27733  climsuse  27734  stoweidlem14  27763  stoweidlem16  27765  stoweidlem20  27769  stoweidlem24  27773  stoweidlem31  27780  stoweidlem34  27783  stoweidlem35  27784  stoweidlem37  27786  stoweidlem39  27788  stoweidlem46  27795  stoweidlem48  27797  stoweidlem51  27800  stoweidlem54  27803  stoweidlem57  27806  stoweidlem59  27808  stoweidlem62  27811  wallispilem3  27816  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  wallispi2  27822  stirlinglem7  27829  stirlinglem12  27834  ndmaovcl  28063  ndmaovcom  28065  ndmaovass  28066  ndmaovdistr  28067  nbgra0edg  28147  uvtx01vtx  28164  tpid3gVD  28618  en3lplem2VD  28620  bnj23  28744  bnj158  28757  bnj168  28758  bnj1138  28820  bnj1143  28822  bnj1454  28874  bnj110  28890  bnj882  28958  bnj893  28960  bnj916  28965  bnj970  28979  bnj983  28983  bnj984  28984  bnj1137  29025  bnj1174  29033  bnj1388  29063  bnj1398  29064  dath  29925  diclspsn  31384  dvh4dimlem  31633  dvh2dim  31635  dvh3dim3N  31639  lcfrvalsnN  31731  mapdh6eN  31930  mapdh7dN  31940  mapdh8b  31970  hdmap1l6e  32005
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator