Theorem eqeltrrd 1164

Description: Deduction that substitutes equal classes into membership.

Hypotheses

Ref	Expression
eqeltrrd.1	⊢ (φ → A = B)
eqeltrrd.2	⊢ (φ → A ∈ C)

Assertion

Ref	Expression
eqeltrrd	⊢ (φ → B ∈ C)

Proof of Theorem eqeltrrd

Step	Hyp	Ref	Expression
1		eqeltrrd.1	. . 3 ⊢ (φ → A = B)
2	1	cleqcomd 1106	. 2 ⊢ (φ → B = A)
3		eqeltrrd.2	. 2 ⊢ (φ → A ∈ C)
4	2, 3	eqeltrd 1163	1 ⊢ (φ → B ∈ C)

Syntax hints:   → wi 2   = wceq 1091   ∈ wcel 1092

This theorem is referenced by:  reucl 1957  tz7.7 2224  inf3lem7 3470  nndiv 4453  zrevaddclt 4592  qrevaddclt 4648  om2uzran 4655  shsel1t 5286  5oalem1 5544  5oalem5 5548  3oalem2 5553

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-cleq 1097  df-clel 1099

metamath.org