HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem eleq1i 1529
Description: Inference from equality to equivalence of membership.
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 1526 . 2 |- (A = B -> (A e. C <-> B e. C))
31, 2ax-mp 7 1 |- (A e. C <-> B e. C)
Colors of variables: wff set class
Syntax hints:   <-> wb 146   = wceq 953   e. wcel 955
This theorem is referenced by:  eleq12i 1531  eqeltr 1536  intexrab 2722  reucl 2875  pwexb 2898  ordtri3or 2969  sucexb 3038  xpsspw 3247  inelv 3346  fressnfv 3823  tz7.48-3 3943  f1stres 4077  f2ndres 4078  elxp6 4086  2on 4123  qsexg 4278  fiint 4534  r1pw 4658  zorn2lem4 4763  alephprc 4865  addclprlem2 5091  distrlem1pr 5099  distrlem2pr 5100  supsrlem5 5201  axicn 5242  pnfnre 5468  mnfnre 5469  nn0subt 6108  nnesq 6592  cnpfval 7697  fsumcnlem 7923  sspval 8316  pilem3 8592  grothprimlem 8721  avril1 8723  hhph 8966  nonbool 9513  pjss2 9542  atssmat 10213  cmphmp 10408  fillsb 10435  rdmob 10525  ishgrag 10605  hgrablkcard 10610
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465
Copyright terms: Public domain