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

Theorem eleq2i 2360
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 2357 . 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 1632    e. wcel 1696
This theorem is referenced by:  eleq12i  2361  eleqtri  2368  eleq2s  2388  hbxfreq  2399  abeq2i  2403  abeq1i  2404  nfceqi  2428  raleqbii  2586  rexeqbii  2587  rabeq2i  2798  elab2g  2929  elrabf  2935  elrab2  2938  cbvsbc  3032  elin2  3372  dfnul2  3470  noel  3472  eltpg  3689  tpid3g  3754  elunirab  3856  elintrab  3890  disjxiun  4036  exss  4252  elop  4255  brabsb  4292  brabga  4295  pofun  4346  elsuci  4474  elsucg  4475  elsuc2g  4476  suceloni  4620  elxp  4722  brab2a  4754  opeliunxp  4756  brab2ga  4779  elcnv  4874  elrnmptg  4945  opelres  4976  rninxp  5133  elfv  5539  fv01  5575  dffv2  5608  fvopab3g  5614  fvmptex  5626  f0cli  5687  fmptco  5707  funfvima  5769  elunirn  5793  fliftel  5824  eloprabga  5950  elrnmpt2  5973  ovid  5980  offval  6101  1st2val  6161  2nd2val  6162  fsplit  6239  xporderlem  6242  brtpos2  6256  fvopab5  6305  opabiota  6309  issmo  6381  smores3  6386  tfrlem7  6415  tfrlem9  6417  tfrlem9a  6418  tfr2b  6428  tfr2  6430  rdgsuc  6453  frsucmptn  6467  tz7.48-2  6470  el1o  6514  dif1o  6515  ondif2  6517  oawordeulem  6568  elecg  6714  brecop  6767  erovlem  6770  eceqoveq  6779  ovec  6784  mapsncnv  6830  mptelixpg  6869  brsdom  6900  isfi  6901  enssdom  6902  brdom2  6907  map1  6955  xpcomco  6968  brsdom2  7001  cnfcom2lem  7420  epfrs  7429  en3lplem2  7433  r1limg  7459  r1ord  7468  r1ord3  7470  tz9.12lem3  7477  rankvaln  7487  r1elss  7494  rankpwi  7511  ssrankr1  7523  r1val3  7526  r1pw  7533  rankr1b  7552  isnum2  7594  cardprclem  7628  infxpenlem  7657  alephcard  7713  alephnbtwn  7714  alephnbtwn2  7715  alephord2  7719  alephsdom  7729  dfac3  7764  dfac5lem2  7767  dfac5lem3  7768  dfac5lem5  7770  pwsdompw  7846  cfub  7891  cardcf  7894  cflecard  7895  cfle  7896  cflim2  7905  cofsmo  7911  cfidm  7917  isfin3  7938  isfin5  7941  isfin6  7942  sdom2en01  7944  fin23lem26  7967  fin23lem30  7984  isf32lem5  7999  itunitc1  8062  ituniiun  8064  axdc3lem2  8093  axdc3lem3  8094  axcclem  8099  axdclem  8162  iunfo  8177  iundom2g  8178  cardidg  8186  konigthlem  8206  alephadd  8215  alephreg  8220  pwcfsdom  8221  cfpwsdom  8222  elgch  8260  fpwwe2lem12  8279  canth4  8285  wunex2  8376  r1tskina  8420  elni  8516  nlt1pi  8546  adderpq  8596  mulerpq  8597  recmulnq  8604  opelcn  8767  opelreal  8768  elreal  8769  elreal2  8770  0ncn  8771  addcnsr  8773  mulcnsr  8774  xrlenlt  8906  elnn0  9983  elnnne0  9995  un0addcl  10013  un0mulcl  10014  uztrn2  10261  elnnuz  10280  elnn0uz  10281  elq  10334  elxr  10474  elfzm1b  10876  uzrdgfni  11037  fzennn  11046  ser0  11114  iswrd  11431  zsum  12207  sumz  12211  sumss  12213  fsumcvg3  12218  abscvgcvg  12293  isumshft  12314  ruclem6  12529  divides  12549  sadc0  12661  eulerthlem2  12866  4sqlem2  13012  4sqlem12  13019  vdwpc  13043  xpscf  13484  cidpropd  13629  oppcsect  13692  funcpropd  13790  natpropd  13866  arwhoma  13893  eldmcoa  13913  pospo  14123  psss  14339  ismnd  14385  ghmeqker  14725  cntri  14822  oppgsubg  14852  efgsfo  15064  efgrelexlemb  15075  lt6abl  15197  dmdprd  15252  dprdval  15254  dprdw  15261  isnirred  15498  isrhm  15517  issrng  15631  lspexchn2  15900  lspindp2l  15903  lspindp2  15904  lbsextlem2  15928  evlslem4  16261  ply1bascl2  16301  eltopspOLD  16672  istpsOLD  16674  istps  16690  mretopd  16845  lpdifsn  16891  restcls  16927  perfopn  16931  pnfnei  16966  mnfnei  16967  lmss  17042  hauscmplem  17149  is2ndc  17188  2ndcdisj  17198  hausnlly  17235  txuni2  17276  ptpjpre1  17282  elpt  17283  dfac14  17328  xkococn  17370  fbasrn  17595  fin1aufil  17643  elfm2  17659  elfm3  17661  fbflim  17687  flffbas  17706  cnpflf2  17711  fclsbas  17732  tsmssubm  17841  imasdsf1olem  17953  isnghm  18248  opnreen  18352  iccpnfcnv  18458  minveclem3b  18808  ovoliunlem1  18877  ioombl1lem4  18934  subopnmbl  18975  vitalilem2  18980  vitalilem3  18981  mbfimaopnlem  19026  mbfimaopn2  19028  itg2l  19100  dvply1  19680  vieta1lem1  19706  vieta1lem2  19707  elaa  19712  taylthlem2  19769  abelthlem6  19828  abelthlem9  19832  sinq34lt0t  19893  ellogrn  19933  dvrelog  20000  ellogdm  20002  logtayl2  20025  cxpcn3lem  20103  cxpcn3  20104  1cubr  20154  atandm  20188  atanf  20192  reasinsin  20208  atans2  20243  dmarea  20268  xrlimcnp  20279  amgmlem  20300  dvdsflip  20438  ppiublem1  20457  lgsdir2lem2  20579  lgsquadlem1  20609  lgsquadlem2  20610  2sqlem1  20618  rpvmasum2  20677  issmgrp  21017  ismndo  21026  isrngo  21061  isdivrngo  21114  isvclem  21149  isnvlem  21182  vsfval  21207  h2hlm  21576  hhcmpl  21795  hhcms  21798  elch0  21849  omlsilem  21997  h1de2ctlem  22150  elspansni  22153  nonbooli  22246  spansncvi  22247  mayete3iOLD  22324  adjeq  22531  cnlnssadj  22676  cnvbraval  22706  ballotlem2  23063  ballotlemfmpn  23069  ballotlem7  23110  ballotth  23112  elxrge02  23132  ssiun3  23172  cntnevol  23191  fmptcof2  23244  fzssnn  23291  xrge0iifcnv  23330  xrge0iifiso  23332  xrge0iifhom  23334  pnfneige0  23389  gsumpropd2lem  23394  logblt  23423  esumnul  23442  measbase  23543  measvuni  23557  ismbfm  23572  elmbfmvol2  23587  isrrvv  23661  coinfliprv  23698  subfacp1lem5  23730  ghomgrpilem2  24008  zprod  24160  prodf1  24165  prod1  24169  elrn3  24191  dfon2lem7  24216  eltrpred  24300  wfrlem5  24331  wfrlem9  24335  wfrlem11  24337  wfrlem12  24338  wfr2  24344  frrlem5  24356  frrlem5e  24360  frrlem11  24364  nofulllem5  24431  elsymdif  24438  brsset  24500  eltrans  24502  elfix  24514  ellimits  24521  elfuns  24525  elsingles  24528  eleenn  24596  fvtransport  24727  brcolinear2  24753  fvray  24836  linedegen  24838  fvline  24839  ellines  24847  bpolydiflem  24861  bpoly2  24864  bpoly3  24865  bpoly4  24866  elhf  24876  hfninf  24888  ftc1cnnc  25025  prmapcp2  25260  isoriso  25315  supaub  25376  supwlub  25377  geme2  25378  isdir2  25395  cbvprodi  25415  zintdom  25541  vecval1b  25554  vecval3b  25555  muldisc  25584  osneisi  25634  islimrs  25683  islimrs3  25684  islimrs4  25685  ismgra  25813  isalg  25824  algi  25830  isded  25839  dedi  25840  rdmob  25851  dmrngcmp  25854  iscatOLD  25857  cati  25858  idmon  25920  cinvlem3  25933  idsubidsup  25960  idsubfun  25961  propsrc  25971  isntr  25976  islimcat  25979  cmp2morpcats  26064  cmp2morpdom  26067  cmpidmor2  26072  clscnc  26113  bisig0  26165  isibcg  26294  fnessref  26396  sdclem2  26555  sdclem1  26556  fdc  26558  caushft  26580  pellex  27023  rmspecnonsq  27095  islmodfg  27270  dsmmelbas  27308  lindsind2  27392  islindf4  27411  aaitgo  27470  pmtrfrn  27503  matrcl  27569  climsuselem1  27836  climsuse  27837  stoweidlem14  27866  stoweidlem16  27868  stoweidlem20  27872  stoweidlem24  27876  stoweidlem31  27883  stoweidlem34  27886  stoweidlem35  27887  stoweidlem37  27889  stoweidlem39  27891  stoweidlem46  27898  stoweidlem48  27900  stoweidlem51  27903  stoweidlem54  27906  stoweidlem57  27909  stoweidlem59  27911  stoweidlem62  27914  wallispilem3  27919  wallispi  27922  wallispi2lem1  27923  wallispi2lem2  27924  wallispi2  27925  stirlinglem7  27932  stirlinglem12  27937  ndmaovcl  28171  ndmaovcom  28173  ndmaovass  28174  ndmaovdistr  28175  nbgra0edg  28281  uvtx01vtx  28305  trlonprop  28341  tpid3gVD  28934  en3lplem2VD  28936  bnj23  29060  bnj158  29073  bnj168  29074  bnj1138  29136  bnj1143  29138  bnj1454  29190  bnj110  29206  bnj882  29274  bnj893  29276  bnj916  29281  bnj970  29295  bnj983  29299  bnj984  29300  bnj1137  29341  bnj1174  29349  bnj1388  29379  bnj1398  29380  dath  30547  diclspsn  32006  dvh4dimlem  32255  dvh2dim  32257  dvh3dim3N  32261  lcfrvalsnN  32353  mapdh6eN  32552  mapdh7dN  32562  mapdh8b  32592  hdmap1l6e  32627
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