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

Theorem eleq1i 2906
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 2903 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538  wcel 2115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-clel 2896
This theorem is referenced by:  eleq12i  2908  eqneltri  2909  eqeltri  2912  intexrab  5229  abssexg  5270  rmorabex  5339  xpsspw  5669  dfse2  5950  ordtri3or  6210  fressnfv  6913  fnotovb  7199  ovmpos  7291  abnex  7473  sucexb  7518  f1stres  7708  f2ndres  7709  elxp6  7718  ottpos  7898  dftpos4  7907  tfr2b  8028  tz7.48-3  8076  difinf  8785  fiint  8792  infssuni  8812  fsuppunbi  8851  r1pwALT  9272  djuexb  9335  alephprc  9523  fin1a2lem12  9831  axcclem  9877  zorn2lem4  9919  zornn0g  9925  grothomex  10249  grothprimlem  10253  addclprlem2  10437  axicn  10570  0mnnnnn0  11926  pfxccatin12lem3  14094  pfxccat3  14096  swrdccat  14097  pfxccat3a  14100  swrdccat3blem  14101  swrdccat3b  14102  harmonic  15214  nprmi  16031  issubm  17968  idresefmnd  18064  mulgfval  18226  oppgsubm  18490  idrespermg  18539  issrg  19257  srgfcl  19265  opprsubrg  19556  resubdrg  20304  cpmidpmat  21484  kgencn  22167  kgencn2  22168  txdis1cn  22246  qtopres  22309  qtopcn  22325  cfinfil  22504  tgphaus  22728  xmeterval  23045  blval2  23175  metuel2  23178  iscvsp  23739  zclmncvs  23759  caucfil  23893  resscdrg  23968  finiunmbl  24154  iblre  24403  logno1  25233  rlimcnp2  25558  ppi2i  25760  gausslemma2dlem1a  25955  2lgslem4  25996  usgredgffibi  27120  nbupgrel  27141  nbuhgr2vtx1edgb  27148  nbusgreledg  27149  nbusgrf1o0  27165  nb3grpr  27178  nb3grpr2  27179  nb3gr2nb  27180  cusgrsizeinds  27248  cusgrfi  27254  finsumvtxdg2size  27346  wlkp1lem1  27469  wlkp1lem7  27475  wlkp1lem8  27476  wwlks2onsym  27750  rusgrnumwwlks  27766  clwwlknclwwlkdifnum  27771  clwwlknonfin  27885  clwwlknonex2  27900  umgr3cyclex  27974  eupthp1  28007  eupth2eucrct  28008  frcond3  28060  frgr3v  28066  3vfriswmgr  28069  1to3vfriendship  28072  2pthfrgrrn  28073  3cyclfrgrrn1  28076  4cycl2v2nb  28080  frgrnbnb  28084  frgrncvvdeqlem3  28092  frgrncvvdeqlem6  28095  frgrhash2wsp  28123  fusgr2wsp2nb  28125  numclwwlk1  28152  avril1  28254  n0lplig  28272  hhph  28967  nonbooli  29440  pjss2i  29469  atssma  30167  isrrext  31301  hasheuni  31404  dmvlsiga  31448  measiuns  31536  eulerpartlemmf  31693  cusgr3cyclex  32443  resconn  32553  cvmlift2lem9  32618  rdgprc0  33098  noxp1o  33230  bj-snsetex  34346  bj-tagex  34370  bj-0int  34464  poimirlem30  35035  ftc1anclem3  35080  ftc1anclem6  35083  rrnheibor  35223  rngo1cl  35325  isdrngo1  35342  dfcoeleqvrels  35964  islpln2ah  36793  lhpocnel2  37263  cdlemg31b0N  37938  cdlemg31b0a  37939  cdlemh  38061  cdlemk19w  38216  3lexlogpow5ineq2  39293  mzpclval  39586  wopprc  39891  dfac21  39930  binomcxplemdvsum  40983  binomcxp  40985  mccl  42170  fprodcn  42172  stoweidlem17  42589  fourierdlem89  42767  fourierdlem90  42768  fourierdlem91  42769  fourierdlem100  42778  omeiunltfirp  43088  hoidmvlelem5  43168  issmf  43292  issmff  43298  smflimlem4  43337  smflim  43340  smflim2  43367  smflimsuplem1  43381  smflimsuplem8  43388  smflimsup  43389  aiotaexb  43576  aiotavb  43577  aovvdm  43671  aovvfunressn  43673  aovrcl  43675  aovvoveq  43678  aov0nbovbi  43681  fnotaovb  43684  prmdvdsfmtnof1lem1  44031  341fppr2  44182  9fppr8  44185  issubmgm  44339  zlmodzxzldeplem3  44841  itscnhlinecirc02p  45129
  Copyright terms: Public domain W3C validator