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

Theorem eleq1i 2531
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 2528 . 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 189    = wceq 1455    e. wcel 1898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-cleq 2455  df-clel 2458
This theorem is referenced by:  eleq12i  2533  eqeltri  2536  intexrab  4579  abssexg  4605  rmorabex  4677  xpsspw  4970  dfse2  5224  ordtri3or  5478  fressnfv  6107  fnotovb  6361  ovmpt2s  6452  snnex  6629  pwexb  6634  sucexb  6668  iprc  6760  f1stres  6847  f2ndres  6848  elxp6  6857  ottpos  7014  dftpos4  7023  tfr2b  7145  tz7.48-3  7192  difinf  7872  fiint  7879  infssuni  7896  fsuppunbi  7935  r1pwALT  8348  alephprc  8561  fin1a2lem12  8872  axcclem  8918  zorn2lem4  8960  zornn0g  8966  grothomex  9285  grothprimlem  9289  addclprlem2  9473  axicn  9605  pnfnre  9713  mnfnre  9714  0mnnnnn0  10936  swrdccatin12lem3  12889  swrdccat3  12891  swrdccat  12892  swrdccat3blem  12894  swrdccat3b  12895  harmonic  13972  nprmi  14694  prmrec  14921  issubm  16649  oppgsubm  17068  idrespermg  17107  issrg  17796  opprsubrg  18084  00lsp  18259  resubdrg  19231  cpmidpmat  19952  kgencn  20626  kgencn2  20627  txdis1cn  20705  qtopres  20768  qtopcn  20784  cfinfil  20963  tgphaus  21186  xmeterval  21502  blval2  21632  metuel2  21635  caucfil  22308  resscdrg  22380  finiunmbl  22553  iblre  22807  logno1  23637  rlimcnp2  23948  ppi2i  24152  nbgrasym  25223  nbgraf1olem3  25227  nbgraf1olem5  25229  nb3grapr  25237  nb3grapr2  25238  nb3gra2nb  25239  cusgra2v  25246  cusgra3v  25248  uvtxnbgra  25277  uvtxnb  25281  cusconngra  25460  2wlkonotv  25661  rusgrasn  25729  frisusgranb  25781  frgra3v  25786  3vfriswmgra  25789  1to3vfriendship  25792  2pthfrgrarn  25793  3cyclfrgrarn1  25796  4cycl2v2nb  25800  frgranbnb  25804  frgrancvvdeqlem2  25815  frgrancvvdeqlem4  25817  frgrancvvdeqlem7  25820  frgrawopreglem4  25831  frgrawopreg  25833  frgrawopreg2  25835  usg2spot2nb  25849  numclwwlkovf2ex  25870  avril1  25956  rngo1cl  26213  hhph  26887  nonbooli  27360  pjss2i  27389  atssma  28087  isrrext  28855  hasheuni  28957  dmvlsiga  29002  measiuns  29090  eulerpartlemmf  29258  rescon  30019  cvmlift2lem9  30084  rdgprc0  30490  bj-snsetex  31603  bj-tagex  31627  bj-pinftynrr  31710  bj-minftynrr  31714  poimirlem30  32016  ftc1anclem3  32065  ftc1anclem6  32068  rrnheibor  32215  isdrngo1  32241  islpln2ah  33160  lhpocnel2  33630  cdlemg31b0N  34307  cdlemg31b0a  34308  cdlemh  34430  cdlemk19w  34585  mzpclval  35613  wopprc  35931  dfac21  35970  binomcxplemdvsum  36749  binomcxp  36751  mccl  37764  stoweidlem17  37978  fourierdlem89  38160  fourierdlem90  38161  fourierdlem91  38162  fourierdlem100  38171  omeiunltfirp  38448  hoidmvlelem5  38528  aovvdm  38822  aovvfunressn  38824  aovrcl  38826  aovvoveq  38829  aov0nbovbi  38832  fnotaovb  38835  pfxccat3  39104  pfxccat3a  39107  nbupgrel  39559  nbuhgr2vtx1edgb  39566  nbusgreledg  39567  nbusgrf1o0  39589  nb3grpr  39602  nb3grpr2  39603  nb3gr2nb  39604  uvtxupgrres  39627  cusgrsizeinds  39659  cusgrfi  39665  umgr3cyclex  40020  issubmgm  40158  zlmodzxzldeplem3  40664
  Copyright terms: Public domain W3C validator