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

Theorem eleqtrd 2429
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eleqtrd.1 (φA B)
eleqtrd.2 (φB = C)
Assertion
Ref Expression
eleqtrd (φA C)

Proof of Theorem eleqtrd
StepHypRef Expression
1 eleqtrd.1 . 2 (φA B)
2 eleqtrd.2 . . 3 (φB = C)
32eleq2d 2420 . 2 (φ → (A BA C))
41, 3mpbid 201 1 (φA C)
Colors of variables: wff setvar class
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:  eleqtrrd  2430  3eltr3d  2433  syl5eleq  2439  syl6eleq  2443  prepeano4  4451  tfinpw1  4494  sfintfin  4532  sfinltfin  4535  fnbr  5185  ecelqsdm  5994  enadjlem1  6059  nenpw1pwlem2  6085  spaccl  6286  fnfreclem3  6319  fnfrec  6320
  Copyright terms: Public domain W3C validator