Theorem eqeltrrd 1546

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 1477	. 2 |- (ph -> B = A)
3		eqeltrrd.2	. 2 |- (ph -> A e. C)
4	2, 3	eqeltrd 1545	1 |- (ph -> B e. C)

Syntax hints:   -> wi 3   = wceq 954   e. wcel 956

This theorem is referenced by:  reucl 2880  tz7.7 2968  xpexr2 3472  dmfex 3646  rnssopab 3816  fopabcos 3824  2ndrn 4100  oneo 4202  inf3lem7 4599  alephfp 4880  cnegextlem2 5326  subopr 5350  resubclt 5418  0re 5420  nndivt 5914  nn0nnaddclt 6081  zsubclt 6123  zrevaddclt 6125  qsubclt 6218  qrevaddclt 6221  om2uzran 6245  icoshftf1oi 6350  peano2uzr 6388  uzaddclt 6389  reim0t 6719  absf 6851  seq1ub 6857  faclbnd6 6899  permnnt 6919  serzclt 6991  serzreclt 6996  serzsplit 7002  fsum0diaglem2 7200  cjcncf 7221  reeff1 7358  istps2 7557  bastopt 7583  metidcn 7852  fsumcnlem 7939  ablmul 8083  ghgrpilem4 8088  vcoprne 8150  ipval2lem3 8302  ipval2lem6 8308  ipf 8313  ip1cnilem2 8321  ip1cnilem3 8322  ubthlem6 8478  minveclem16 8504  minveclem37 8525  sincolem 8603  relogclt 8698  hhshsslem2 9077  pjocclt 9204  shsel1t 9223  5oalem1 9539  5oalem5 9543  3oalem2 9548  hmopdt 9885  adjsslnop 9958  bracnlnvalt 9985  pjhmopidm 10048  cayleylem2 10344  filintf 10479  rcmob 10562  isfuna 10628

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-cleq 1467  df-clel 1470

Copyright terms: Public domain