Theorem eqeltrd 2427

Description: Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)

Hypotheses

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

Assertion

Ref	Expression
eqeltrd	⊢ (φ → A ∈ C)

Proof of Theorem eqeltrd

Step	Hyp	Ref	Expression
1		eqeltrd.2	. 2 ⊢ (φ → B ∈ C)
2		eqeltrd.1	. . 3 ⊢ (φ → A = B)
3	2	eleq1d 2419	. 2 ⊢ (φ → (A ∈ C ↔ B ∈ C))
4	1, 3	mpbird 223	1 ⊢ (φ → A ∈ C)

Syntax hints:   → wi 4   = wceq 1642   ∈ wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346  df-clel 2349

This theorem is referenced by:  eqeltrrd  2428  3eltr4d  2434  syl5eqel  2437  syl6eqel  2441  ifclda  3690  intab  3957  nnsucelr  4429  ssfin  4471  tfinprop  4490  vfintle  4547  vfinspclt  4553  vinf  4556  ideqg  4869  dffo3  5423  f1oiso2  5501  elimdelov  5574  fvmptd  5703  enmap2lem5  6068  enmap1lem5  6074  ncssfin  6152  nntccl  6171