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

Theorem eleq1i 2534
Description: Inference from equality to equivalence of membership. (Contributed by NM, 21-Jun-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 2529 . 2  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
31, 2ax-mp 5 1  |-  ( A  e.  C  <->  B  e.  C )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1395    e. wcel 1819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-cleq 2449  df-clel 2452
This theorem is referenced by:  eleq12i  2536  eqeltri  2541  intexrab  4615  abssexg  4641  rmorabex  4716  ordtri3or  4919  xpsspwOLD  5126  dfse2  5380  fressnfv  6086  fnotovb  6337  ovmpt2s  6425  snnex  6605  pwexb  6610  sucexb  6643  iprc  6734  f1stres  6821  f2ndres  6822  elxp6  6831  ottpos  6983  dftpos4  6992  tfr2b  7083  tz7.48-3  7127  difinf  7808  fiint  7815  infssuni  7829  fsuppunbi  7868  oef1oOLD  8159  r1pwALT  8281  alephprc  8497  fin1a2lem12  8808  axcclem  8854  zorn2lem4  8896  zornn0g  8902  grothomex  9224  grothprimlem  9228  addclprlem2  9412  axicn  9544  pnfnre  9652  mnfnre  9653  0mnnnnn0  10849  swrdccatin12lem3  12726  swrdccat3  12728  swrdccat  12729  swrdccat3blem  12731  swrdccat3b  12732  harmonic  13681  nprmi  14243  prmrec  14451  issubm  16104  oppgsubm  16523  idrespermg  16562  issrg  17285  opprsubrg  17576  00lsp  17753  funsnfsupOLD  18382  resubdrg  18770  cpmidpmat  19500  kgencn  20182  kgencn2  20183  txdis1cn  20261  qtopres  20324  qtopcn  20340  cfinfil  20519  tgphaus  20740  xmeterval  21060  blval2  21203  metuel2  21207  caucfil  21847  resscdrg  21923  finiunmbl  22079  iblre  22325  logno1  23142  rlimcnp2  23421  ppi2i  23568  nbgrasym  24565  nbgraf1olem3  24569  nbgraf1olem5  24571  nb3grapr  24579  nb3grapr2  24580  nb3gra2nb  24581  cusgra2v  24588  cusgra3v  24590  uvtxnbgra  24619  uvtxnb  24623  cusconngra  24802  2wlkonotv  25003  rusgrasn  25071  frisusgranb  25123  frgra3v  25128  3vfriswmgra  25131  1to3vfriendship  25134  2pthfrgrarn  25135  3cyclfrgrarn1  25138  4cycl2v2nb  25142  frgranbnb  25146  frgrancvvdeqlem2  25157  frgrancvvdeqlem4  25159  frgrancvvdeqlem7  25162  frgrawopreglem4  25173  frgrawopreg  25175  frgrawopreg2  25177  usg2spot2nb  25191  numclwwlkovf2ex  25212  avril1  25297  rngo1cl  25557  hhph  26221  nonbooli  26695  pjss2i  26724  atssma  27423  isrrext  28134  hasheuni  28247  dmvlsiga  28290  measiuns  28349  eulerpartlemmf  28489  rescon  28866  cvmlift2lem9  28931  rdgprc0  29400  ftc1anclem3  30254  ftc1anclem6  30257  rrnheibor  30495  isdrngo1  30521  mzpclval  30819  wopprc  31134  dfac21  31174  binomcxplemdvsum  31422  binomcxp  31424  mccl  31767  stoweidlem17  31960  fourierdlem89  32139  fourierdlem90  32140  fourierdlem91  32141  fourierdlem100  32150  aovvdm  32431  aovvfunressn  32433  aovrcl  32435  aovvoveq  32438  aov0nbovbi  32441  fnotaovb  32444  pfxccat3  32502  pfxccat3a  32505  issubmgm  32697  zlmodzxzldeplem3  33205  bj-snsetex  34622  bj-tagex  34646  bj-pinftynrr  34726  bj-minftynrr  34730  islpln2ah  35374  lhpocnel2  35844  cdlemg31b0N  36521  cdlemg31b0a  36522  cdlemh  36644  cdlemk19w  36799
  Copyright terms: Public domain W3C validator