Theorem eleq1i 1797

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

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 |- A = B
2		eleq1 1794	. 2 |- (A = B -> (A e. C <-> B e. C))
3	1, 2	ax-mp 7	1 |- (A e. C <-> B e. C)

Syntax hints:   <-> wb 162   = wceq 1136   e. wcel 1138

This theorem is referenced by:  eleq12i 1799  eqeltri 1804  reucl 3035  intexrab 3283  pwex 3302  abssexg 3305  ordtri3or 3506  ordtri3orOLD 3507  snnex 3612  pwexb 3663  sucexb 3701  xpsspw 3904  iprc 4021  fressnfv 4624  f1stres 4845  f2ndres 4846  elxp6 4852  tz7.48-3 4978  2onOLD 4995  qsexg 5163  undefnel2 5369  fiint 5460  pwfilem 5470  ordtypelem4 5497  r1pw 5606  zorn2lem4 5749  alephprc 5837  addclprlem2 6067  distrlem1pr 6075  distrlem2pr 6076  supsrlem5 6177  axicn 6219  pnfnre 6461  mnfnre 6462  nn0sub 7165  nnesqi 7707  cnpfval 8828  fsumcnlem 9062  nvoprne 9433  sspval 9516  pilem3 9817  grothprimlem 9935  avril1 9937  islfin 9962  fiuni 10012  hmeobc 10031  fsubbas 10073  sfvlim 10088  ring1cl 10207  zrdivrng 10210  hhph 10470  nonbooli 11023  pjss2i 11052  atssma 11742  4nprm 13573  isunscov 14116  fldrels 14178  npincppr 14227  islatalg 14257  inpc 14343  toplat 14364  vecval3b 14518  cmphmp 14598  bwt2 14674  rdmob 14777  dualded 14814  dualcat2 14815  issubcat 14875  tartwo 14915  elfiun 15051  fictb 15053  ordtypelem4OLD 15060  ufinffr 15260  inficl 15439  zornn0 15446  mettrifi 15529  heiborlem26 15662  heiborlem29 15665  heiborlem41 15677  rrnheibor 15705  isdivrng1 15791  ishgrag 15973  hgrablkcard 15978  isdivrngNEW 16889

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1143  ax-17 1155  ax-4 1157  ax-5o 1159  ax-ext 1702

This theorem depends on definitions:  df-bi 163  df-an 241  df-ex 1165  df-cleq 1714  df-clel 1717

Copyright terms: Public domain