Theorem eqeltrrd 1549

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

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

This theorem is referenced by:  reucl 2885  tz7.7 2973  xpexr2 3480  dmfex 3655  rnssopab 3825  fopabcos 3833  2ndrn 4110  oneo 4212  inf3lem7 4619  alephfp 4900  cnegextlem2 5346  subopr 5370  resubclt 5438  0re 5440  nndivt 5959  nn0nnaddclt 6126  zsubclt 6168  zrevaddclt 6170  qsubclt 6272  qrevaddclt 6275  om2uzran 6300  icoshftf1oi 6409  peano2uzr 6448  uzaddclt 6449  reim0t 6774  rerebt 6776  absf 6906  seq1ub 6912  faclbnd6 6954  permnnt 6973  serzclt 7045  serzreclt 7050  serzsplit 7056  fsum0diaglem2 7257  cjcncf 7278  reeff1 7410  istps2 7607  bastopt 7633  metidcn 7900  fsumcnlem 7989  ablmul 8131  ghgrpilem4 8136  vcoprne 8198  ipval2lem3 8355  ipval2lem6 8361  ipf 8366  ip1cnilem2 8374  ip1cnilem3 8375  ubthlem6 8534  minveclem16 8560  minveclem37 8581  sincolem 8665  relogclt 8759  hhshsslem2 9138  pjocclt 9266  shsel1t 9285  5oalem1 9599  5oalem5 9603  3oalem2 9608  hmopdt 9947  adjsslnop 10020  bracnlnvalt 10047  pjhmopidm 10110  cayleylem2 10410  filintf 10569  rcmob 10682  isfuna 10754

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain