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

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

Proof of Theorem eleq1i
StepHypRef Expression
1 eleq1i.1 . 2  |-  A  =  B
2 eleq1 2343 . 2  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
31, 2ax-mp 8 1  |-  ( A  e.  C  <->  B  e.  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    e. wcel 1684
This theorem is referenced by:  eleq12i  2348  eqeltri  2353  intexrab  4170  abssexg  4195  rmorabex  4233  ordtri3or  4424  snnex  4524  pwexb  4564  sucexb  4600  xpsspwOLD  4798  iprc  4943  dfse2  5046  fressnfv  5707  fnotovb  5894  f1stres  6141  f2ndres  6142  elxp6  6151  ottpos  6244  dftpos4  6253  tfr2b  6412  tz7.48-3  6456  difinf  7127  fiint  7133  oef1o  7401  r1pwOLD  7518  alephprc  7726  fin1a2lem12  8037  axcclem  8083  zorn2lem4  8126  zornn0g  8132  grothomex  8451  grothprimlem  8455  addclprlem2  8641  axicn  8772  pnfnre  8874  mnfnre  8875  harmonic  12317  nprmi  12773  prmrec  12969  issubm  14425  oppgsubm  14835  opprsubrg  15566  00lsp  15738  kgencn  17251  kgencn2  17252  txdis1cn  17329  qtopres  17389  qtopcn  17405  cfinfil  17588  tgphaus  17799  xmeterval  17978  caucfil  18709  resscdrg  18775  finiunmbl  18901  iblre  19148  logno1  19983  rlimcnp2  20261  ppi2i  20407  avril1  20836  rngo1cl  21096  hhph  21757  nonbooli  22230  pjss2i  22259  atssma  22958  elovimad  23205  hasheuni  23453  sigaex  23470  sigaclfu2  23482  dmvlsiga  23490  prsiga  23492  inelsiga  23496  brsiga  23514  measiuns  23544  measinb2  23550  mbfmcnt  23573  coinflipprob  23680  coinfliprv  23683  rescon  23777  cvmlift2lem9  23842  rdgprc0  24150  isunscov  25074  islatalg  25183  inpc  25277  toplat  25290  vecval3b  25452  islimrs4  25582  bwt2  25592  rdmob  25748  issubcata  25846  prismorcset2  25918  domcatfun  25925  codcatfun  25934  rrnheibor  26561  isdrngo1  26587  funsnfsup  26762  mzpclval  26803  wopprc  27123  dfac21  27164  rfcnpre1  27690  stoweidlem16  27765  stoweidlem17  27766  stoweidlem18  27767  stoweidlem57  27806  stoweidlem59  27808  aovvdm  28045  aovvfunressn  28047  aovrcl  28049  aovvoveq  28052  aov0nbovbi  28055  fnotaovb  28058  nbgrasym  28152  cusgra2v  28158  uvtxnbgra  28165  frgra3v  28180  3vfriswmgra  28183  1to3vfriendship  28186  islpln2ah  29738  lhpocnel2  30208  cdlemg31b0N  30883  cdlemg31b0a  30884  cdlemh  31006  cdlemk19w  31161
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