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

Theorem eleq2i 2468
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 2465 . 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 177    = wceq 1649    e. wcel 1721
This theorem is referenced by:  eleq12i  2469  eleqtri  2476  eleq2s  2496  hbxfreq  2507  abeq2i  2511  abeq1i  2512  nfceqi  2536  raleqbii  2696  rexeqbii  2697  rabeq2i  2913  elab2g  3044  elrabf  3051  elrab2  3054  cbvsbc  3149  elin2  3491  dfnul2  3590  noel  3592  eltpg  3811  tpid3g  3879  elunirab  3988  elintrab  4022  disjxiun  4169  exss  4386  elop  4389  brabsb  4426  brabga  4429  pofun  4479  elsuci  4607  elsucg  4608  elsuc2g  4609  suceloni  4752  elxp  4854  brab2a  4886  opeliunxp  4888  brab2ga  4910  elcnv  5008  elrnmptg  5079  opelres  5110  rninxp  5269  elfv  5685  fv01  5722  dffv2  5755  fvopab3g  5761  fvmptex  5774  f0cli  5839  fmptco  5860  funfvima  5932  elunirn  5957  fliftel  5990  eloprabga  6119  elrnmpt2  6142  ovid  6149  offval  6271  1st2val  6331  2nd2val  6332  bropopvvv  6385  fsplit  6410  xporderlem  6416  brtpos2  6444  fvopab5  6493  opabiota  6497  issmo  6569  smores3  6574  tfrlem7  6603  tfrlem9  6605  tfrlem9a  6606  tfr2b  6616  tfr2  6618  rdgsuc  6641  frsucmptn  6655  tz7.48-2  6658  el1o  6702  dif1o  6703  ondif2  6705  oawordeulem  6756  elecg  6902  brecop  6956  erovlem  6959  eceqoveq  6968  ovec  6973  mapsncnv  7019  mptelixpg  7058  brsdom  7089  isfi  7090  enssdom  7091  brdom2  7096  map1  7144  xpcomco  7157  brsdom2  7190  cnfcom2lem  7614  epfrs  7623  en3lplem2  7627  r1limg  7653  r1ord  7662  r1ord3  7664  tz9.12lem3  7671  rankvaln  7681  r1elss  7688  rankpwi  7705  ssrankr1  7717  r1val3  7720  r1pw  7727  rankr1b  7746  isnum2  7788  cardprclem  7822  infxpenlem  7851  alephcard  7907  alephnbtwn  7908  alephnbtwn2  7909  alephord2  7913  alephsdom  7923  dfac3  7958  dfac5lem2  7961  dfac5lem3  7962  dfac5lem5  7964  pwsdompw  8040  cfub  8085  cardcf  8088  cflecard  8089  cfle  8090  cflim2  8099  cofsmo  8105  cfidm  8111  isfin3  8132  isfin5  8135  isfin6  8136  sdom2en01  8138  fin23lem26  8161  fin23lem30  8178  isf32lem5  8193  itunitc1  8256  ituniiun  8258  axdc3lem2  8287  axdc3lem3  8288  axcclem  8293  axdclem  8355  iunfo  8370  iundom2g  8371  cardidg  8379  konigthlem  8399  alephadd  8408  alephreg  8413  pwcfsdom  8414  cfpwsdom  8415  elgch  8453  fpwwe2lem12  8472  canth4  8478  wunex2  8569  r1tskina  8613  elni  8709  nlt1pi  8739  adderpq  8789  mulerpq  8790  recmulnq  8797  opelcn  8960  opelreal  8961  elreal  8962  elreal2  8963  0ncn  8964  addcnsr  8966  mulcnsr  8967  xrlenlt  9099  elnn0  10179  elnnne0  10191  un0addcl  10209  un0mulcl  10210  uztrn2  10459  elnnuz  10478  elnn0uz  10479  elq  10532  elxr  10672  elfzm1b  11080  uzrdgfni  11253  fzennn  11262  ser0  11330  iswrd  11684  zsum  12467  sumz  12471  sumss  12473  fsumcvg3  12478  abscvgcvg  12553  isumshft  12574  ruclem6  12789  divides  12809  sadc0  12921  eulerthlem2  13126  4sqlem2  13272  4sqlem12  13279  vdwpc  13303  xpscf  13746  cidpropd  13891  oppcsect  13954  funcpropd  14052  natpropd  14128  arwhoma  14155  eldmcoa  14175  pospo  14385  psss  14601  ismnd  14647  ghmeqker  14987  cntri  15084  oppgsubg  15114  efgsfo  15326  efgrelexlemb  15337  lt6abl  15459  dmdprd  15514  dprdval  15516  dprdw  15523  isnirred  15760  isrhm  15779  issrng  15893  lspexchn2  16158  lspindp2l  16161  lspindp2  16162  lbsextlem2  16186  evlslem4  16519  ply1bascl2  16557  eltopspOLD  16938  istpsOLD  16940  istps  16956  mretopd  17111  neiptopuni  17149  lpdifsn  17162  restcls  17199  perfopn  17203  pnfnei  17238  mnfnei  17239  lmss  17316  hauscmplem  17423  is2ndc  17462  2ndcdisj  17472  hausnlly  17509  txuni2  17550  ptpjpre1  17556  elpt  17557  dfac14  17603  xkococn  17645  fbasrn  17869  fin1aufil  17917  elfm2  17933  elfm3  17935  fbflim  17961  flffbas  17980  cnpflf2  17985  fclsbas  18006  tsmssubm  18125  iscusp2  18285  imasdsf1olem  18356  metustelOLD  18534  metustel  18535  metuel2  18562  isnghm  18710  opnreen  18815  iccpnfcnv  18922  minveclem3b  19282  ovoliunlem1  19351  ioombl1lem4  19408  subopnmbl  19449  vitalilem2  19454  vitalilem3  19455  mbfimaopnlem  19500  mbfimaopn2  19502  itg2l  19574  dvply1  20154  vieta1lem1  20180  vieta1lem2  20181  elaa  20186  taylthlem2  20243  abelthlem6  20305  abelthlem9  20309  sinq34lt0t  20370  ellogrn  20410  dvrelog  20481  ellogdm  20483  logtayl2  20506  cxpcn3lem  20584  cxpcn3  20585  1cubr  20635  atandm  20669  atanf  20673  reasinsin  20689  atans2  20724  dmarea  20749  xrlimcnp  20760  amgmlem  20781  dvdsflip  20920  ppiublem1  20939  lgsdir2lem2  21061  lgsquadlem1  21091  lgsquadlem2  21092  2sqlem1  21100  rpvmasum2  21159  nbgra0edg  21397  nbgraf1olem1  21404  nbgraf1olem3  21406  nbgraf1olem5  21408  uvtx01vtx  21454  issmgrp  21875  ismndo  21884  isrngo  21919  isdivrngo  21972  isvclem  22009  isnvlem  22042  vsfval  22067  h2hlm  22436  hhcmpl  22655  hhcms  22658  elch0  22709  omlsilem  22857  h1de2ctlem  23010  elspansni  23013  nonbooli  23106  spansncvi  23107  mayete3iOLD  23184  adjeq  23391  cnlnssadj  23536  cnvbraval  23566  fmptcof2  24029  ofpreima  24034  1stpreima  24048  2ndpreima  24049  elxrge02  24131  gsumpropd2lem  24173  xrge0iifcnv  24272  xrge0iifiso  24274  xrge0iifhom  24276  pnfneige0  24289  qqhre  24339  rrhre  24340  esumnul  24396  measvuni  24521  cntnevol  24535  dya2iocnrect  24584  sibf0  24602  isrrvv  24654  coinfliprv  24693  ballotlem7  24746  subfacp1lem5  24823  ghomgrpilem2  25050  prodf1  25172  zprod  25216  prod1  25223  prodss  25226  prodsn  25239  elrn3  25334  dfon2lem7  25359  eltrpred  25443  wfrlem9  25478  wfrlem11  25480  wfrlem12  25481  wfr2  25487  frrlem5e  25503  frrlem11  25507  nofulllem5  25574  elsymdif  25581  brsset  25643  eltrans  25645  elfix  25657  ellimits  25664  elfuns  25668  elsingles  25671  eleenn  25739  fvtransport  25870  brcolinear2  25896  fvray  25979  linedegen  25981  fvline  25982  ellines  25990  bpolydiflem  26004  bpoly2  26007  bpoly3  26008  bpoly4  26009  elhf  26019  hfninf  26031  cnambfre  26154  ftc1cnnc  26178  fnessref  26263  sdclem2  26336  sdclem1  26337  fdc  26339  caushft  26357  pellex  26788  rmspecnonsq  26860  islmodfg  27035  dsmmelbas  27073  lindsind2  27157  islindf4  27176  aaitgo  27235  pmtrfrn  27268  climsuselem1  27600  climsuse  27601  stoweidlem14  27630  stoweidlem39  27655  stoweidlem48  27664  stoweidlem51  27667  stoweidlem59  27675  stoweidlem62  27678  wallispilem3  27683  ndmaovcl  27934  ndmaovcom  27936  ndmaovass  27937  ndmaovdistr  27938  otiunsndisj  27954  otiunsndisjX  27955  swrdccatin2  28018  2wlkonot3v  28072  2spthonot3v  28073  frgranbnb  28124  frgrancvvdeqlem2  28134  frgrancvvdeqlem3  28135  frgrancvvdeqlem4  28136  frgrancvvdeqlemC  28142  frgrawopreglem3  28149  frgrawopreglem4  28150  frgrawopreg  28152  2spotiundisj  28165  tpid3gVD  28663  en3lplem2VD  28665  bnj23  28789  bnj158  28802  bnj168  28803  bnj1138  28865  bnj1143  28867  bnj1454  28919  bnj110  28935  bnj882  29003  bnj893  29005  bnj916  29010  bnj970  29024  bnj983  29028  bnj984  29029  bnj1137  29070  bnj1174  29078  bnj1388  29108  bnj1398  29109  dath  30218  diclspsn  31677  dvh4dimlem  31926  dvh2dim  31928  dvh3dim3N  31932  lcfrvalsnN  32024  mapdh6eN  32223  mapdh7dN  32233  mapdh8b  32263  hdmap1l6e  32298
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