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

Theorem eleq1i 2359
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 2356 . 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 1632    e. wcel 1696
This theorem is referenced by:  eleq12i  2361  eqeltri  2366  intexrab  4186  abssexg  4211  rmorabex  4249  ordtri3or  4440  snnex  4540  pwexb  4580  sucexb  4616  xpsspwOLD  4814  iprc  4959  dfse2  5062  fressnfv  5723  fnotovb  5910  f1stres  6157  f2ndres  6158  elxp6  6167  ottpos  6260  dftpos4  6269  tfr2b  6428  tz7.48-3  6472  difinf  7143  fiint  7149  oef1o  7417  r1pwOLD  7534  alephprc  7742  fin1a2lem12  8053  axcclem  8099  zorn2lem4  8142  zornn0g  8148  grothomex  8467  grothprimlem  8471  addclprlem2  8657  axicn  8788  pnfnre  8890  mnfnre  8891  harmonic  12333  nprmi  12789  prmrec  12985  issubm  14441  oppgsubm  14851  opprsubrg  15582  00lsp  15754  kgencn  17267  kgencn2  17268  txdis1cn  17345  qtopres  17405  qtopcn  17421  cfinfil  17604  tgphaus  17815  xmeterval  17994  caucfil  18725  resscdrg  18791  finiunmbl  18917  iblre  19164  logno1  19999  rlimcnp2  20277  ppi2i  20423  avril1  20852  rngo1cl  21112  hhph  21773  nonbooli  22246  pjss2i  22275  atssma  22974  elovimad  23220  hasheuni  23468  sigaex  23485  sigaclfu2  23497  dmvlsiga  23505  prsiga  23507  inelsiga  23511  brsiga  23529  measiuns  23559  measinb2  23565  mbfmcnt  23588  coinflipprob  23695  coinfliprv  23698  rescon  23792  cvmlift2lem9  23857  rdgprc0  24221  isunscov  25177  islatalg  25286  inpc  25380  toplat  25393  vecval3b  25555  islimrs4  25685  bwt2  25695  rdmob  25851  issubcata  25949  prismorcset2  26021  domcatfun  26028  codcatfun  26037  rrnheibor  26664  isdrngo1  26690  funsnfsup  26865  mzpclval  26906  wopprc  27226  dfac21  27267  rfcnpre1  27793  stoweidlem16  27868  stoweidlem17  27869  stoweidlem18  27870  stoweidlem57  27909  stoweidlem59  27911  aovvdm  28153  aovvfunressn  28155  aovrcl  28157  aovvoveq  28160  aov0nbovbi  28163  fnotaovb  28166  nbgrasym  28286  nb3grapr  28289  nb3grapr2  28290  nb3gra2nb  28291  cusgra2v  28297  cusgra3v  28299  uvtxnbgra  28306  frgra3v  28426  3vfriswmgra  28429  1to3vfriendship  28432  2pthfrgrarn  28433  3cyclfrgrarn1  28435  4cycl2v2nb  28438  islpln2ah  30360  lhpocnel2  30830  cdlemg31b0N  31505  cdlemg31b0a  31506  cdlemh  31628  cdlemk19w  31783
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