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

Theorem eleq1i 2501
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 2498 . 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 178    = wceq 1653    e. wcel 1726
This theorem is referenced by:  eleq12i  2503  eqeltri  2508  intexrab  4361  abssexg  4386  rmorabex  4425  ordtri3or  4615  snnex  4715  pwexb  4755  sucexb  4791  xpsspwOLD  4989  iprc  5136  dfse2  5239  fressnfv  5922  fnotovb  6119  f1stres  6370  f2ndres  6371  elxp6  6380  ottpos  6491  dftpos4  6500  tfr2b  6659  tz7.48-3  6703  difinf  7379  fiint  7385  infssuni  7399  oef1o  7657  r1pwOLD  7774  alephprc  7982  fin1a2lem12  8293  axcclem  8339  zorn2lem4  8381  zornn0g  8387  grothomex  8706  grothprimlem  8710  addclprlem2  8896  axicn  9027  pnfnre  9129  mnfnre  9130  harmonic  12640  nprmi  13096  prmrec  13292  issubm  14750  oppgsubm  15160  opprsubrg  15891  00lsp  16059  bwth  17475  kgencn  17590  kgencn2  17591  txdis1cn  17669  qtopres  17732  qtopcn  17748  cfinfil  17927  tgphaus  18148  xmeterval  18464  blval2  18607  metuel2  18611  caucfil  19238  resscdrg  19314  finiunmbl  19440  iblre  19687  logno1  20529  rlimcnp2  20807  ppi2i  20954  nbgrasym  21451  nbgraf1olem3  21455  nbgraf1olem5  21457  nb3grapr  21464  nb3grapr2  21465  nb3gra2nb  21466  cusgra2v  21473  cusgra3v  21475  uvtxnbgra  21504  cusconngra  21665  avril1  21759  rngo1cl  22019  hhph  22682  nonbooli  23155  pjss2i  23184  atssma  23883  hasheuni  24477  dmvlsiga  24514  measiuns  24573  rescon  24935  cvmlift2lem9  25000  rdgprc0  25423  ftc1anclem3  26284  ftc1anclem6  26287  rrnheibor  26548  isdrngo1  26574  funsnfsup  26745  mzpclval  26784  wopprc  27103  dfac21  27143  stoweidlem17  27744  aovvdm  28027  aovvfunressn  28029  aovrcl  28031  aovvoveq  28034  aov0nbovbi  28037  fnotaovb  28040  0mnnnnn0  28106  swrdccatin12lem4  28235  swrdccat3  28237  swrdccat  28238  swrdccat3blem  28240  swrdccat3b  28241  uvtxnb  28319  2wlkonotv  28397  frisusgranb  28449  frgra3v  28454  3vfriswmgra  28457  1to3vfriendship  28460  2pthfrgrarn  28461  3cyclfrgrarn1  28464  4cycl2v2nb  28468  frgranbnb  28472  frgrancvvdeqlem2  28482  frgrancvvdeqlem4  28484  frgrancvvdeqlem7  28487  frgrawopreglem4  28498  frgrawopreg  28500  frgrawopreg2  28502  usg2spot2nb  28516  islpln2ah  30408  lhpocnel2  30878  cdlemg31b0N  31553  cdlemg31b0a  31554  cdlemh  31676  cdlemk19w  31831
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