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

Theorem eleq1i 2479
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 2474 . 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 1405    e. wcel 1842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-cleq 2394  df-clel 2397
This theorem is referenced by:  eleq12i  2481  eqeltri  2486  intexrab  4553  abssexg  4579  rmorabex  4651  xpsspw  4937  dfse2  5190  ordtri3or  5442  fressnfv  6065  fnotovb  6319  ovmpt2s  6407  snnex  6588  pwexb  6593  sucexb  6627  iprc  6719  f1stres  6806  f2ndres  6807  elxp6  6816  ottpos  6968  dftpos4  6977  tfr2b  7099  tz7.48-3  7146  difinf  7824  fiint  7831  infssuni  7845  fsuppunbi  7884  oef1oOLD  8174  r1pwALT  8296  alephprc  8512  fin1a2lem12  8823  axcclem  8869  zorn2lem4  8911  zornn0g  8917  grothomex  9237  grothprimlem  9241  addclprlem2  9425  axicn  9557  pnfnre  9665  mnfnre  9666  0mnnnnn0  10869  swrdccatin12lem3  12771  swrdccat3  12773  swrdccat  12774  swrdccat3blem  12776  swrdccat3b  12777  harmonic  13822  nprmi  14441  prmrec  14649  issubm  16302  oppgsubm  16721  idrespermg  16760  issrg  17479  opprsubrg  17770  00lsp  17947  funsnfsupOLD  18576  resubdrg  18942  cpmidpmat  19666  kgencn  20349  kgencn2  20350  txdis1cn  20428  qtopres  20491  qtopcn  20507  cfinfil  20686  tgphaus  20907  xmeterval  21227  blval2  21370  metuel2  21374  caucfil  22014  resscdrg  22090  finiunmbl  22246  iblre  22492  logno1  23311  rlimcnp2  23622  ppi2i  23824  nbgrasym  24856  nbgraf1olem3  24860  nbgraf1olem5  24862  nb3grapr  24870  nb3grapr2  24871  nb3gra2nb  24872  cusgra2v  24879  cusgra3v  24881  uvtxnbgra  24910  uvtxnb  24914  cusconngra  25093  2wlkonotv  25294  rusgrasn  25362  frisusgranb  25414  frgra3v  25419  3vfriswmgra  25422  1to3vfriendship  25425  2pthfrgrarn  25426  3cyclfrgrarn1  25429  4cycl2v2nb  25433  frgranbnb  25437  frgrancvvdeqlem2  25448  frgrancvvdeqlem4  25450  frgrancvvdeqlem7  25453  frgrawopreglem4  25464  frgrawopreg  25466  frgrawopreg2  25468  usg2spot2nb  25482  numclwwlkovf2ex  25503  avril1  25588  rngo1cl  25845  hhph  26509  nonbooli  26983  pjss2i  27012  atssma  27710  isrrext  28433  hasheuni  28532  dmvlsiga  28577  measiuns  28665  eulerpartlemmf  28820  rescon  29543  cvmlift2lem9  29608  rdgprc0  30013  bj-snsetex  31086  bj-tagex  31110  bj-pinftynrr  31189  bj-minftynrr  31193  ftc1anclem3  31465  ftc1anclem6  31468  rrnheibor  31615  isdrngo1  31641  islpln2ah  32566  lhpocnel2  33036  cdlemg31b0N  33713  cdlemg31b0a  33714  cdlemh  33836  cdlemk19w  33991  mzpclval  35019  wopprc  35334  dfac21  35374  binomcxplemdvsum  36108  binomcxp  36110  mccl  36974  stoweidlem17  37167  fourierdlem89  37346  fourierdlem90  37347  fourierdlem91  37348  fourierdlem100  37357  aovvdm  37638  aovvfunressn  37640  aovrcl  37642  aovvoveq  37645  aov0nbovbi  37648  fnotaovb  37651  pfxccat3  37913  pfxccat3a  37916  issubmgm  38106  zlmodzxzldeplem3  38614
  Copyright terms: Public domain W3C validator