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

Theorem eleq1i 2528
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 2523 . 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 1370    e. wcel 1758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2443  df-clel 2446
This theorem is referenced by:  eleq12i  2530  eqeltri  2535  intexrab  4551  abssexg  4577  rmorabex  4652  ordtri3or  4851  xpsspwOLD  5054  dfse2  5302  fressnfv  5997  fnotovb  6230  ovmpt2s  6316  snnex  6484  pwexb  6489  sucexb  6522  iprc  6615  f1stres  6700  f2ndres  6701  elxp6  6710  ottpos  6857  dftpos4  6866  tfr2b  6957  tz7.48-3  7001  difinf  7685  fiint  7691  infssuni  7705  fsuppunbi  7744  oef1oOLD  8034  r1pwOLD  8156  alephprc  8372  fin1a2lem12  8683  axcclem  8729  zorn2lem4  8771  zornn0g  8777  grothomex  9099  grothprimlem  9103  addclprlem2  9289  axicn  9420  pnfnre  9528  mnfnre  9529  0mnnnnn0  10715  swrdccatin12lem3  12485  swrdccat3  12487  swrdccat  12488  swrdccat3blem  12490  swrdccat3b  12491  harmonic  13425  nprmi  13882  prmrec  14087  issubm  15579  oppgsubm  15981  idrespermg  16020  issrg  16716  opprsubrg  16994  00lsp  17170  funsnfsupOLD  17779  resubdrg  18149  bwthOLD  19132  kgencn  19247  kgencn2  19248  txdis1cn  19326  qtopres  19389  qtopcn  19405  cfinfil  19584  tgphaus  19805  xmeterval  20125  blval2  20268  metuel2  20272  caucfil  20912  resscdrg  20988  finiunmbl  21143  iblre  21389  logno1  22199  rlimcnp2  22478  ppi2i  22625  nbgrasym  23485  nbgraf1olem3  23489  nbgraf1olem5  23491  nb3grapr  23498  nb3grapr2  23499  nb3gra2nb  23500  cusgra2v  23507  cusgra3v  23509  uvtxnbgra  23538  cusconngra  23699  avril1  23793  rngo1cl  24053  hhph  24717  nonbooli  25191  pjss2i  25220  atssma  25919  isrrext  26565  hasheuni  26670  dmvlsiga  26708  measiuns  26767  eulerpartlemmf  26894  rescon  27271  cvmlift2lem9  27336  rdgprc0  27743  ftc1anclem3  28609  ftc1anclem6  28612  rrnheibor  28876  isdrngo1  28902  mzpclval  29201  wopprc  29519  dfac21  29559  stoweidlem17  29952  aovvdm  30231  aovvfunressn  30233  aovrcl  30235  aovvoveq  30238  aov0nbovbi  30241  fnotaovb  30244  uvtxnb  30418  2wlkonotv  30536  rusgrasn  30697  frisusgranb  30729  frgra3v  30734  3vfriswmgra  30737  1to3vfriendship  30740  2pthfrgrarn  30741  3cyclfrgrarn1  30744  4cycl2v2nb  30748  frgranbnb  30752  frgrancvvdeqlem2  30764  frgrancvvdeqlem4  30766  frgrancvvdeqlem7  30769  frgrawopreglem4  30780  frgrawopreg  30782  frgrawopreg2  30784  usg2spot2nb  30798  numclwwlkovf2ex  30819  mpt2matmul  31018  zlmodzxzldeplem3  31153  cpmidpmat  31329  bj-snsetex  32758  bj-tagex  32782  bj-pinftynrr  32853  bj-minftynrr  32857  islpln2ah  33501  lhpocnel2  33971  cdlemg31b0N  34646  cdlemg31b0a  34647  cdlemh  34769  cdlemk19w  34924
  Copyright terms: Public domain W3C validator