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

Theorem eleq1i 2539
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 2534 . 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 1374    e. wcel 1762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-cleq 2454  df-clel 2457
This theorem is referenced by:  eleq12i  2541  eqeltri  2546  intexrab  4601  abssexg  4627  rmorabex  4702  ordtri3or  4905  xpsspwOLD  5110  dfse2  5363  fressnfv  6068  fnotovb  6316  ovmpt2s  6403  snnex  6579  pwexb  6584  sucexb  6617  iprc  6711  f1stres  6798  f2ndres  6799  elxp6  6808  ottpos  6957  dftpos4  6966  tfr2b  7057  tz7.48-3  7101  difinf  7781  fiint  7788  infssuni  7802  fsuppunbi  7841  oef1oOLD  8133  r1pwOLD  8255  alephprc  8471  fin1a2lem12  8782  axcclem  8828  zorn2lem4  8870  zornn0g  8876  grothomex  9198  grothprimlem  9202  addclprlem2  9386  axicn  9518  pnfnre  9626  mnfnre  9627  0mnnnnn0  10819  swrdccatin12lem3  12667  swrdccat3  12669  swrdccat  12670  swrdccat3blem  12672  swrdccat3b  12673  harmonic  13624  nprmi  14082  prmrec  14290  issubm  15783  oppgsubm  16187  idrespermg  16226  issrg  16944  opprsubrg  17228  00lsp  17405  funsnfsupOLD  18022  resubdrg  18406  mpt2matmul  18710  cpmidpmat  19136  bwthOLD  19672  kgencn  19787  kgencn2  19788  txdis1cn  19866  qtopres  19929  qtopcn  19945  cfinfil  20124  tgphaus  20345  xmeterval  20665  blval2  20808  metuel2  20812  caucfil  21452  resscdrg  21528  finiunmbl  21684  iblre  21930  logno1  22740  rlimcnp2  23019  ppi2i  23166  nbgrasym  24103  nbgraf1olem3  24107  nbgraf1olem5  24109  nb3grapr  24117  nb3grapr2  24118  nb3gra2nb  24119  cusgra2v  24126  cusgra3v  24128  uvtxnbgra  24157  uvtxnb  24161  cusconngra  24340  2wlkonotv  24541  rusgrasn  24609  frisusgranb  24661  frgra3v  24666  3vfriswmgra  24669  1to3vfriendship  24672  2pthfrgrarn  24673  3cyclfrgrarn1  24676  4cycl2v2nb  24680  frgranbnb  24684  frgrancvvdeqlem2  24696  frgrancvvdeqlem4  24698  frgrancvvdeqlem7  24701  frgrawopreglem4  24712  frgrawopreg  24714  frgrawopreg2  24716  usg2spot2nb  24730  numclwwlkovf2ex  24751  avril1  24835  rngo1cl  25095  hhph  25759  nonbooli  26233  pjss2i  26262  atssma  26961  isrrext  27605  hasheuni  27719  dmvlsiga  27757  measiuns  27816  eulerpartlemmf  27942  rescon  28319  cvmlift2lem9  28384  rdgprc0  28791  ftc1anclem3  29658  ftc1anclem6  29661  rrnheibor  29925  isdrngo1  29951  mzpclval  30250  wopprc  30567  dfac21  30607  stoweidlem17  31274  fourierdlem89  31453  fourierdlem90  31454  fourierdlem91  31455  fourierdlem100  31464  aovvdm  31694  aovvfunressn  31696  aovrcl  31698  aovvoveq  31701  aov0nbovbi  31704  fnotaovb  31707  zlmodzxzldeplem3  32061  bj-snsetex  33479  bj-tagex  33503  bj-pinftynrr  33574  bj-minftynrr  33578  islpln2ah  34222  lhpocnel2  34692  cdlemg31b0N  35367  cdlemg31b0a  35368  cdlemh  35490  cdlemk19w  35645
  Copyright terms: Public domain W3C validator