New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  eqeltrd GIF version

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
StepHypRef Expression
1 eqeltrd.2 . 2 (φB C)
2 eqeltrd.1 . . 3 (φA = B)
32eleq1d 2419 . 2 (φ → (A CB C))
41, 3mpbird 223 1 (φA C)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1642   ∈ wcel 1710 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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  3689  intab  3956  nnsucelr  4428  ssfin  4470  tfinprop  4489  vfintle  4546  vfinspclt  4552  vinf  4555  ideqg  4868  dffo3  5422  f1oiso2  5500  elimdelov  5573  fvmptd  5702  enmap2lem5  6067  enmap1lem5  6073  ncssfin  6151  nntccl  6170
 Copyright terms: Public domain W3C validator