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

Theorem eleqtrrd 2219
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 2145 . 2 (𝜑𝐵 = 𝐶)
41, 3eleqtrd 2218 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1331  wcel 1480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  3eltr4d  2223  exmidsssnc  4126  tfrexlem  6231  nnsucuniel  6391  erref  6449  en1uniel  6698  fin0  6779  fin0or  6780  prarloclemarch2  7239  fzopth  9853  fzoss2  9961  fzosubel3  9985  elfzomin  9995  elfzonlteqm1  9999  fzoend  10011  fzofzp1  10016  fzofzp1b  10017  peano2fzor  10021  zmodfzo  10132  frecuzrdg0  10198  frecuzrdgsuc  10199  frecuzrdgdomlem  10202  frecuzrdg0t  10207  frecuzrdgsuctlem  10208  seq3f1olemqsum  10285  bcn2  10522  summodclem2a  11162  fisumss  11173  fsumm1  11197  fisumcom2  11219  prodmodclem2a  11357  ennnfonelemex  11938  ctinfomlemom  11951  lmtopcnp  12433  txopn  12448  blpnfctr  12622  metcnpi  12698  metcnpi2  12699  cncfmpt2fcntop  12768  limcimolemlt  12816  cnplimclemr  12821  limccnp2lem  12828  limccnp2cntop  12829  dvidlemap  12843  dvcnp2cntop  12846  dvcn  12847  dvaddxxbr  12848  dvmulxxbr  12849  dvef  12871
  Copyright terms: Public domain W3C validator