Theorem eleq1i 1580

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 1577	. 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 144   = wceq 992   e. wcel 994

This theorem is referenced by:  eleq12i 1582  eqeltri 1587  reucl 2584  intexrab 2806  ordtri3or 3007  snnex 3100  pwexb 3131  sucexb 3166  xpsspw 3346  iprc 3449  fressnfv 3952  f1stres 4154  f2ndres 4155  elxp6 4161  tz7.48-3 4259  2on 4275  qsexg 4434  fiint 4703  pwfilem 4713  r1pw 4832  zorn2lem4 4937  alephprc 5043  addclprlem2 5273  distrlem1pr 5281  distrlem2pr 5282  supsrlem5 5383  axicn 5424  pnfnre 5650  mnfnre 5651  nn0sub 6329  nnesqi 6863  cnpfval 7967  fsumcnlem 8200  nvoprne 8553  sspval 8636  pilem3 8940  grothprimlem 9056  avril1 9058  hhph 9321  nonbooli 9874  pjss2i 9903  atssma 10587  isunscov 10796  islfin 10799  islatalg 10831  inpc 10867  toplat 10884  ring1cl 10966  zrdivrng 10969  cmphmp 11027  hmeobc 11048  sfvlim 11100  bwt2 11123  rdmob 11202  issubcat 11299  fiuni 11420  elfiun 11421  fictb 11423  ordtypelem4 11430  fsubbas 11630  ufinffr 11663  inficl 11849  mettrifi 11912  heiborlem26 12036  heiborlem29 12039  heiborlem41 12051  rrnheibor 12079  ishgrag 12195  hgrablkcard 12200

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-cleq 1511  df-clel 1514

Copyright terms: Public domain