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

Theorem eleqtrrd 2164
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eleqtrrd.1 (𝜑𝐴𝐵)
eleqtrrd.2 (𝜑𝐶 = 𝐵)
Assertion
Ref Expression
eleqtrrd (𝜑𝐴𝐶)

Proof of Theorem eleqtrrd
StepHypRef Expression
1 eleqtrrd.1 . 2 (𝜑𝐴𝐵)
2 eleqtrrd.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2090 . 2 (𝜑𝐵 = 𝐶)
41, 3eleqtrd 2163 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  wcel 1436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081
This theorem is referenced by:  3eltr4d  2168  tfrexlem  6053  nnsucuniel  6210  erref  6264  en1uniel  6473  fin0  6553  fin0or  6554  prarloclemarch2  6922  fzopth  9406  fzoss2  9511  fzosubel3  9535  elfzomin  9545  elfzonlteqm1  9549  fzoend  9561  fzofzp1  9566  fzofzp1b  9567  peano2fzor  9571  zmodfzo  9682  frecuzrdg0  9748  frecuzrdgsuc  9749  frecuzrdgdomlem  9752  frecuzrdg0t  9757  frecuzrdgsuctlem  9758  iseqf1olemqsum  9833  bcn2  10068  isummolem2a  10660  fisumss  10670
  Copyright terms: Public domain W3C validator