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

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

Proof of Theorem eleqtrrd
StepHypRef Expression
1 eleqtrrd.1 . 2 (φA B)
2 eleqtrrd.2 . . 3 (φ𝐶 = B)
32eqcomd 2042 . 2 (φB = 𝐶)
41, 3eleqtrd 2113 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:  3eltr4d  2118  tfrexlem  5889  erref  6062  en1uniel  6220  prarloclemarch2  6402  fzopth  8694  fzoss2  8798  fzosubel3  8822  elfzomin  8832  elfzonlteqm1  8836  fzoend  8848  fzofzp1  8853  fzofzp1b  8854  peano2fzor  8858  frecuzrdgcl  8880  frecuzrdg0  8881  frecuzrdgsuc  8882
  Copyright terms: Public domain W3C validator