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

Theorem eleq1i 2678
Description: Inference from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
eleq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
eleq1i (𝐴𝐶𝐵𝐶)

Proof of Theorem eleq1i
StepHypRef Expression
1 eleq1i.1 . 2 𝐴 = 𝐵
2 eleq1 2675 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wcel 1976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2602  df-clel 2605
This theorem is referenced by:  eleq12i  2680  eqeltri  2683  intexrab  4745  abssexg  4772  rmorabex  4849  xpsspw  5145  dfse2  5405  ordtri3or  5658  fressnfv  6310  fnotovb  6570  ovmpt2s  6660  snnex  6839  pwexb  6844  sucexb  6878  iprc  6970  f1stres  7058  f2ndres  7059  elxp6  7068  ottpos  7226  dftpos4  7235  tfr2b  7356  tz7.48-3  7403  difinf  8092  fiint  8099  infssuni  8117  fsuppunbi  8156  r1pwALT  8569  alephprc  8782  fin1a2lem12  9093  axcclem  9139  zorn2lem4  9181  zornn0g  9187  grothomex  9507  grothprimlem  9511  addclprlem2  9695  axicn  9827  pnfnre  9937  mnfnre  9938  0mnnnnn0  11172  swrdccatin12lem3  13287  swrdccat3  13289  swrdccat  13290  swrdccat3blem  13292  swrdccat3b  13293  harmonic  14376  nprmi  15186  prmrec  15410  issubm  17116  oppgsubm  17561  idrespermg  17600  issrg  18276  srgfcl  18284  opprsubrg  18570  00lsp  18748  resubdrg  19718  cpmidpmat  20439  kgencn  21111  kgencn2  21112  txdis1cn  21190  qtopres  21253  qtopcn  21269  cfinfil  21449  tgphaus  21672  xmeterval  21988  blval2  22118  metuel2  22121  iscvsp  22665  caucfil  22807  resscdrg  22879  finiunmbl  23036  iblre  23283  logno1  24099  rlimcnp2  24410  ppi2i  24612  gausslemma2dlem1a  24807  2lgslem4  24848  nbgrasym  25734  nbgraf1olem3  25738  nbgraf1olem5  25740  nb3grapr  25748  nb3grapr2  25749  nb3gra2nb  25750  cusgra2v  25757  cusgra3v  25759  uvtxnbgra  25787  uvtxnb  25791  cusconngra  25970  2wlkonotv  26170  rusgrasn  26238  frisusgranb  26290  frgra3v  26295  3vfriswmgra  26298  1to3vfriendship  26301  2pthfrgrarn  26302  3cyclfrgrarn1  26305  4cycl2v2nb  26309  frgranbnb  26313  frgrancvvdeqlem2  26324  frgrancvvdeqlem4  26326  frgrancvvdeqlem7  26329  frgrawopreglem4  26340  frgrawopreg  26342  frgrawopreg2  26344  usg2spot2nb  26358  numclwwlkovf2ex  26379  avril1  26477  hhph  27225  nonbooli  27700  pjss2i  27729  atssma  28427  isrrext  29178  hasheuni  29280  dmvlsiga  29325  measiuns  29413  eulerpartlemmf  29570  rescon  30288  cvmlift2lem9  30353  rdgprc0  30749  bj-snsetex  31940  bj-tagex  31964  bj-pinftynrr  32082  bj-minftynrr  32086  poimirlem30  32405  ftc1anclem3  32453  ftc1anclem6  32456  rrnheibor  32602  rngo1cl  32704  isdrngo1  32721  islpln2ah  33649  lhpocnel2  34119  cdlemg31b0N  34796  cdlemg31b0a  34797  cdlemh  34919  cdlemk19w  35074  mzpclval  36102  wopprc  36411  dfac21  36450  binomcxplemdvsum  37372  binomcxp  37374  mccl  38462  fprodcn  38464  stoweidlem17  38707  fourierdlem89  38885  fourierdlem90  38886  fourierdlem91  38887  fourierdlem100  38896  omeiunltfirp  39206  hoidmvlelem5  39286  issmf  39411  issmff  39417  smflimlem4  39457  smflim  39460  aovvdm  39712  aovvfunressn  39714  aovrcl  39716  aovvoveq  39719  aov0nbovbi  39722  fnotaovb  39725  prmdvdsfmtnof1lem1  39832  pfxccat3  40087  pfxccat3a  40090  nbupgrel  40562  nbuhgr2vtx1edgb  40569  nbusgreledg  40570  nbusgrf1o0  40592  nb3grpr  40605  nb3grpr2  40606  nb3gr2nb  40607  cusgrsizeinds  40663  cusgrfi  40669  1wlkp1lem1  40877  1wlkp1lem7  40883  1wlkp1lem8  40884  rusgrnumwwlks  41172  clwwlknclwwlkdifnum  41177  umgr3cyclex  41345  eupthp1  41379  eupth2eucrct  41380  frcond3  41435  frgr3v  41440  3vfriswmgr  41443  1to3vfriendship-av  41446  2pthfrgrrn  41447  3cyclfrgrrn1  41450  4cycl2v2nb-av  41454  frgrnbnb  41458  frgrncvvdeqlem2  41465  frgrncvvdeqlem4  41467  frgrncvvdeqlem7  41470  frgrwopreglem4  41479  frgrwopreg  41481  frgrwopreg2  41483  frgr2wwlkeqm  41491  frgrhash2wsp  41492  av-numclwwlkffin  41507  av-numclwwlkovf2ex  41512  issubmgm  41574  zlmodzxzldeplem3  42080
  Copyright terms: Public domain W3C validator