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

Theorem eleq1i 2829
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 2826 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-clel 2815
This theorem is referenced by:  eleq12i  2831  eqeltri  2834  eqneltri  2857  intexrab  5302  abssexg  5342  rmorabex  5422  otelxp  5681  xpsspw  5770  dfse2  6057  dfse3  6295  ordtri3or  6354  fressnfv  7111  fnotovb  7412  ovmpos  7508  abnex  7696  sucexb  7744  f1stres  7950  f2ndres  7951  elxp6  7960  ottpos  8172  dftpos4  8181  tfr2b  8347  tz7.48-3  8395  unfi  9123  difinf  9267  fiint  9275  infssuni  9294  fsuppunbi  9333  r1pwALT  9789  djuexb  9852  alephprc  10042  fin1a2lem12  10354  axcclem  10400  zorn2lem4  10442  zornn0g  10448  grothomex  10772  grothprimlem  10776  addclprlem2  10960  axicn  11093  0mnnnnn0  12452  fcdmnn0fsupp  12477  pfxccatin12lem3  14627  pfxccat3  14629  swrdccat  14630  pfxccat3a  14633  swrdccat3blem  14634  swrdccat3b  14635  harmonic  15751  nprmi  16572  issubm  18621  idresefmnd  18716  mulgfval  18881  oppgsubm  19150  idrespermg  19200  issrg  19926  srgfcl  19934  opprsubrg  20259  resubdrg  21028  cpmidpmat  22238  kgencn  22923  kgencn2  22924  txdis1cn  23002  qtopres  23065  qtopcn  23081  cfinfil  23260  tgphaus  23484  xmeterval  23801  blval2  23934  metuel2  23937  iscvsp  24507  zclmncvs  24528  caucfil  24663  resscdrg  24738  finiunmbl  24924  iblre  25174  logno1  26007  rlimcnp2  26332  ppi2i  26534  gausslemma2dlem1a  26729  2lgslem4  26770  noxp1o  27027  usgredgffibi  28314  nbupgrel  28335  nbuhgr2vtx1edgb  28342  nbusgreledg  28343  nbusgrf1o0  28359  nb3grpr  28372  nb3grpr2  28373  nb3gr2nb  28374  cusgrsizeinds  28442  cusgrfi  28448  finsumvtxdg2size  28540  wlkp1lem1  28663  wlkp1lem7  28669  wlkp1lem8  28670  wwlks2onsym  28945  rusgrnumwwlks  28961  clwwlknclwwlkdifnum  28966  clwwlknonfin  29080  clwwlknonex2  29095  umgr3cyclex  29169  eupthp1  29202  eupth2eucrct  29203  frcond3  29255  frgr3v  29261  3vfriswmgr  29264  1to3vfriendship  29267  2pthfrgrrn  29268  3cyclfrgrrn1  29271  4cycl2v2nb  29275  frgrnbnb  29279  frgrncvvdeqlem3  29287  frgrncvvdeqlem6  29290  frgrhash2wsp  29318  fusgr2wsp2nb  29320  numclwwlk1  29347  avril1  29449  n0lplig  29467  hhph  30162  nonbooli  30635  pjss2i  30664  atssma  31362  isrrext  32621  hasheuni  32724  dmvlsiga  32768  measiuns  32856  eulerpartlemmf  33015  fineqvrep  33736  cusgr3cyclex  33770  resconn  33880  cvmlift2lem9  33945  rdgprc0  34407  bj-snsetex  35463  bj-tagex  35487  bj-0int  35601  poimirlem30  36137  ftc1anclem3  36182  ftc1anclem6  36185  rrnheibor  36325  rngo1cl  36427  isdrngo1  36444  dfcoeleqvrels  37112  islpln2ah  38041  lhpocnel2  38511  cdlemg31b0N  39186  cdlemg31b0a  39187  cdlemh  39309  cdlemk19w  39464  aks4d1lem1  40548  sticksstones4  40586  mzpclval  41077  wopprc  41383  dfac21  41422  uniel  41580  sucomisnotcard  41890  binomcxplemdvsum  42709  binomcxp  42711  mccl  43913  fprodcn  43915  stoweidlem17  44332  fourierdlem89  44510  fourierdlem90  44511  fourierdlem91  44512  fourierdlem100  44521  omeiunltfirp  44834  hoidmvlelem5  44914  issmf  45043  issmff  45049  smflimlem4  45089  smflim  45092  smflim2  45121  smflimsuplem1  45135  smflimsuplem8  45142  smflimsup  45143  aiotaexb  45395  aiotavb  45396  aovvdm  45491  aovvfunressn  45493  aovrcl  45495  aovvoveq  45498  aov0nbovbi  45501  fnotaovb  45504  prmdvdsfmtnof1lem1  45850  341fppr2  46000  9fppr8  46003  issubmgm  46157  zlmodzxzldeplem3  46657  itscnhlinecirc02p  46945
  Copyright terms: Public domain W3C validator