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

Theorem eleq2i 2502
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 2499 . 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 178    = wceq 1653    e. wcel 1726
This theorem is referenced by:  eleq12i  2503  eleqtri  2510  eleq2s  2530  hbxfreq  2541  abeq2i  2545  abeq1i  2546  nfceqi  2570  raleqbii  2737  rexeqbii  2738  rabeq2i  2955  elab2g  3086  elrabf  3093  elrab2  3096  cbvsbc  3191  elin2  3533  dfnul2  3632  noel  3634  eltpg  3853  tpid3g  3921  elunirab  4030  elintrab  4064  disjxiun  4211  exss  4428  elop  4431  brabsb  4468  brabga  4471  pofun  4521  elsuci  4649  elsucg  4650  elsuc2g  4651  suceloni  4795  elxp  4897  brab2a  4929  opeliunxp  4931  brab2ga  4953  elcnv  5051  elrnmptg  5122  opelres  5153  rninxp  5312  elfv  5728  fv01  5765  dffv2  5798  fvopab3g  5804  fvmptex  5817  f0cli  5882  fmptco  5903  funfvima  5975  elunirn  6000  fliftel  6033  eloprabga  6162  elrnmpt2  6185  ovid  6192  offval  6314  1st2val  6374  2nd2val  6375  bropopvvv  6428  fsplit  6453  xporderlem  6459  brtpos2  6487  fvopab5  6536  opabiota  6540  issmo  6612  smores3  6617  tfrlem7  6646  tfrlem9  6648  tfrlem9a  6649  tfr2b  6659  tfr2  6661  rdgsuc  6684  frsucmptn  6698  tz7.48-2  6701  el1o  6745  dif1o  6746  ondif2  6748  oawordeulem  6799  elecg  6945  brecop  6999  erovlem  7002  eceqoveq  7011  ovec  7016  mapsncnv  7062  mptelixpg  7101  brsdom  7132  isfi  7133  enssdom  7134  brdom2  7139  map1  7187  xpcomco  7200  brsdom2  7233  cnfcom2lem  7660  epfrs  7669  en3lplem2  7673  r1limg  7699  r1ord  7708  r1ord3  7710  tz9.12lem3  7717  rankvaln  7727  r1elss  7734  rankpwi  7751  ssrankr1  7763  r1val3  7766  r1pw  7773  rankr1b  7792  isnum2  7834  cardprclem  7868  infxpenlem  7897  alephcard  7953  alephnbtwn  7954  alephnbtwn2  7955  alephord2  7959  alephsdom  7969  dfac3  8004  dfac5lem2  8007  dfac5lem3  8008  dfac5lem5  8010  pwsdompw  8086  cfub  8131  cardcf  8134  cflecard  8135  cfle  8136  cflim2  8145  cofsmo  8151  cfidm  8157  isfin3  8178  isfin5  8181  isfin6  8182  sdom2en01  8184  fin23lem26  8207  fin23lem30  8224  isf32lem5  8239  itunitc1  8302  ituniiun  8304  axdc3lem2  8333  axdc3lem3  8334  axcclem  8339  axdclem  8401  iunfo  8416  iundom2g  8417  cardidg  8425  konigthlem  8445  alephadd  8454  alephreg  8459  pwcfsdom  8460  cfpwsdom  8461  elgch  8499  fpwwe2lem12  8518  canth4  8524  wunex2  8615  r1tskina  8659  elni  8755  nlt1pi  8785  adderpq  8835  mulerpq  8836  recmulnq  8843  opelcn  9006  opelreal  9007  elreal  9008  elreal2  9009  0ncn  9010  addcnsr  9012  mulcnsr  9013  xrlenlt  9145  elnn0  10225  elnnne0  10237  un0addcl  10255  un0mulcl  10256  uztrn2  10505  elnnuz  10524  elnn0uz  10525  elq  10578  elxr  10718  elfzm1b  11127  uzrdgfni  11300  fzennn  11309  ser0  11377  iswrd  11731  zsum  12514  sumz  12518  sumss  12520  fsumcvg3  12525  abscvgcvg  12600  isumshft  12621  ruclem6  12836  divides  12856  sadc0  12968  eulerthlem2  13173  4sqlem2  13319  4sqlem12  13326  vdwpc  13350  xpscf  13793  cidpropd  13938  oppcsect  14001  funcpropd  14099  natpropd  14175  arwhoma  14202  eldmcoa  14222  pospo  14432  psss  14648  ismnd  14694  ghmeqker  15034  cntri  15131  oppgsubg  15161  efgsfo  15373  efgrelexlemb  15384  lt6abl  15506  dmdprd  15561  dprdval  15563  dprdw  15570  isnirred  15807  isrhm  15826  issrng  15940  lspexchn2  16205  lspindp2l  16208  lspindp2  16209  lbsextlem2  16233  evlslem4  16566  ply1bascl2  16604  eltopspOLD  16985  istpsOLD  16987  istps  17003  mretopd  17158  neiptopuni  17196  lpdifsn  17209  restcls  17247  perfopn  17251  pnfnei  17286  mnfnei  17287  lmss  17364  hauscmplem  17471  is2ndc  17511  2ndcdisj  17521  hausnlly  17558  txuni2  17599  ptpjpre1  17605  elpt  17606  dfac14  17652  xkococn  17694  fbasrn  17918  fin1aufil  17966  elfm2  17982  elfm3  17984  fbflim  18010  flffbas  18029  cnpflf2  18034  fclsbas  18055  tsmssubm  18174  iscusp2  18334  imasdsf1olem  18405  metustelOLD  18583  metustel  18584  metuel2  18611  isnghm  18759  opnreen  18864  iccpnfcnv  18971  minveclem3b  19331  ovoliunlem1  19400  ioombl1lem4  19457  subopnmbl  19498  vitalilem2  19503  vitalilem3  19504  mbfimaopnlem  19549  mbfimaopn2  19551  itg2l  19623  dvply1  20203  vieta1lem1  20229  vieta1lem2  20230  elaa  20235  taylthlem2  20292  abelthlem6  20354  abelthlem9  20358  sinq34lt0t  20419  ellogrn  20459  dvrelog  20530  ellogdm  20532  logtayl2  20555  cxpcn3lem  20633  cxpcn3  20634  1cubr  20684  atandm  20718  atanf  20722  reasinsin  20738  atans2  20773  dmarea  20798  xrlimcnp  20809  amgmlem  20830  dvdsflip  20969  ppiublem1  20988  lgsdir2lem2  21110  lgsquadlem1  21140  lgsquadlem2  21141  2sqlem1  21149  rpvmasum2  21208  nbgra0edg  21446  nbgraf1olem1  21453  nbgraf1olem3  21455  nbgraf1olem5  21457  uvtx01vtx  21503  issmgrp  21924  ismndo  21933  isrngo  21968  isdivrngo  22021  isvclem  22058  isnvlem  22091  vsfval  22116  h2hlm  22485  hhcmpl  22704  hhcms  22707  elch0  22758  omlsilem  22906  h1de2ctlem  23059  elspansni  23062  nonbooli  23155  spansncvi  23156  mayete3iOLD  23233  adjeq  23440  cnlnssadj  23585  cnvbraval  23615  fmptcof2  24078  ofpreima  24083  1stpreima  24097  2ndpreima  24098  elxrge02  24180  gsumpropd2lem  24222  xrge0iifcnv  24321  xrge0iifiso  24323  xrge0iifhom  24325  pnfneige0  24338  qqhre  24388  rrhre  24389  esumnul  24445  measvuni  24570  cntnevol  24584  dya2iocnrect  24633  sibf0  24651  isrrvv  24703  coinfliprv  24742  ballotlem7  24795  subfacp1lem5  24872  ghomgrpilem2  25099  prodf1  25221  zprod  25265  prod1  25272  prodss  25275  prodsn  25288  elrn3  25388  dfon2lem7  25418  eltrpred  25506  wfrlem9  25548  wfrlem11  25550  wfrlem12  25551  wfr2  25557  frrlem5e  25592  frrlem11  25596  nofulllem5  25663  elsymdif  25670  brsset  25736  eltrans  25738  elfix  25750  ellimits  25757  elfuns  25762  elsingles  25765  eleenn  25837  fvtransport  25968  brcolinear2  25994  fvray  26077  linedegen  26079  fvline  26080  ellines  26088  bpolydiflem  26102  bpoly2  26105  bpoly3  26106  bpoly4  26107  elhf  26117  hfninf  26129  cnambfre  26257  ftc1cnnc  26281  fnessref  26375  sdclem2  26448  sdclem1  26449  fdc  26451  caushft  26469  pellex  26900  rmspecnonsq  26972  islmodfg  27146  dsmmelbas  27184  lindsind2  27268  islindf4  27287  aaitgo  27346  pmtrfrn  27379  climsuselem1  27711  climsuse  27712  stoweidlem14  27741  stoweidlem39  27766  stoweidlem48  27775  stoweidlem51  27778  stoweidlem59  27786  stoweidlem62  27789  wallispilem3  27794  ndmaovcl  28045  ndmaovcom  28047  ndmaovass  28048  ndmaovdistr  28049  otiunsndisj  28069  otiunsndisjX  28070  elovmpt3rab1  28095  2wlkonot3v  28395  2spthonot3v  28396  isrgra  28429  isrusgra  28430  frgranbnb  28472  frgrancvvdeqlem2  28482  frgrancvvdeqlem3  28483  frgrancvvdeqlem4  28484  frgrancvvdeqlemC  28490  frgrawopreglem3  28497  frgrawopreglem4  28498  frgrawopreg  28500  2spotiundisj  28513  tpid3gVD  29016  en3lplem2VD  29018  bnj23  29145  bnj158  29158  bnj168  29159  bnj1138  29221  bnj1143  29223  bnj1454  29275  bnj110  29291  bnj882  29359  bnj893  29361  bnj916  29366  bnj970  29380  bnj983  29384  bnj984  29385  bnj1137  29426  bnj1174  29434  bnj1388  29464  bnj1398  29465  dath  30595  diclspsn  32054  dvh4dimlem  32303  dvh2dim  32305  dvh3dim3N  32309  lcfrvalsnN  32401  mapdh6eN  32600  mapdh7dN  32610  mapdh8b  32640  hdmap1l6e  32675
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2431  df-clel 2434
  Copyright terms: Public domain W3C validator