Theorem eqeltrrd 1552

Description: Deduction that substitutes equal classes into membership.

Hypotheses

Ref	Expression
eqeltrrd.1	|- (ph -> A = B)
eqeltrrd.2	|- (ph -> A e. C)

Assertion

Ref	Expression
eqeltrrd	|- (ph -> B e. C)

Proof of Theorem eqeltrrd

Step	Hyp	Ref	Expression
1		eqeltrrd.1	. . 3 |- (ph -> A = B)
2	1	eqcomd 1483	. 2 |- (ph -> B = A)
3		eqeltrrd.2	. 2 |- (ph -> A e. C)
4	2, 3	eqeltrd 1551	1 |- (ph -> B e. C)

Syntax hints:   -> wi 3   = wceq 958   e. wcel 960

This theorem is referenced by:  reucl 2892  tz7.7 2980  xpexr2 3487  dmfex 3662  rnssopab 3832  fopabcos 3840  2ndrn 4117  oneo 4219  inf3lem7 4635  alephfp 4918  cnegextlem2 5365  subopr 5389  resubclt 5457  0re 5459  nndivt 5968  nn0nnaddclt 6135  zsubclt 6177  zrevaddclt 6179  qsubclt 6280  qrevaddclt 6283  om2uzran 6308  icoshftf1oi 6417  peano2uzr 6456  uzaddclt 6457  reim0t 6782  rerebt 6784  absf 6913  seq1ub 6919  faclbnd6 6961  permnnt 6980  serzclt 7052  serzreclt 7057  serzsplit 7063  fsum0diaglem2 7264  cjcncf 7285  reeff1 7417  istps2 7615  bastopt 7639  metidcn 7904  fsumcnlem 7993  ablmul 8134  ghgrpilem4 8139  vcoprne 8201  ipval2lem3 8358  ipval2lem6 8364  ipf 8369  ip1cnilem2 8377  ip1cnilem3 8378  ubthlem6 8537  minveclem16 8563  minveclem37 8584  sincolem 8667  relogclt 8761  hhshsslem2 9140  pjocclt 9268  shsel1t 9287  5oalem1 9601  5oalem5 9605  3oalem2 9610  hmopdt 9949  adjsslnop 10022  bracnlnvalt 10049  pjhmopidm 10112  cayleylem2 10413  filintf 10562  rcmob 10661  isfuna 10733

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-cleq 1472  df-clel 1475

Copyright terms: Public domain