ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eleqtrd Structured version   GIF version

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

Proof of Theorem eleqtrd
StepHypRef Expression
1 eleqtrd.1 . 2 (φA B)
2 eleqtrd.2 . . 3 (φB = 𝐶)
32eleq2d 2104 . 2 (φ → (A BA 𝐶))
41, 3mpbid 135 1 (φA 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242   wcel 1390
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033
This theorem is referenced by:  eleqtrrd  2114  3eltr3d  2117  syl5eleq  2123  syl6eleq  2127  opth1  3964  0nelop  3976  tfisi  4253  ercl  6053  erth  6086  ecelqsdm  6112  lincmb01cmp  8621  fzopth  8674  fzoaddel2  8799  fzosubel2  8801  fzocatel  8805  zpnn0elfzo1  8814  fzoend  8828  peano2fzor  8838
  Copyright terms: Public domain W3C validator