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

Theorem eqeltrd 2111
Description: Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
Hypotheses
Ref Expression
eqeltrd.1 (φA = B)
eqeltrd.2 (φB 𝐶)
Assertion
Ref Expression
eqeltrd (φA 𝐶)

Proof of Theorem eqeltrd
StepHypRef Expression
1 eqeltrd.2 . 2 (φB 𝐶)
2 eqeltrd.1 . . 3 (φA = B)
32eleq1d 2103 . 2 (φ → (A 𝐶B 𝐶))
41, 3mpbird 156 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:  eqeltrrd  2112  3eltr4d  2118  syl5eqel  2121  syl6eqel  2125  intab  3635  iinexgm  3899  opexg  3955  opexgOLD  3956  tfisi  4253  imain  4924  fvmptd  5196  fvmptdf  5201  fvmptt  5205  dffo3  5257  resfunexg  5325  f1oiso2  5409  riota2df  5431  riota5f  5435  ovmpt2dxf  5568  ovmpt2df  5574  offval  5661  iunexg  5688  oprabexd  5696  fo1stresm  5730  fo2ndresm  5731  1stdm  5750  1stconst  5784  2ndconst  5785  cnvf1olem  5787  fo2ndf  5790  iunon  5840  tfrlemibacc  5881  tfrlemibfn  5883  frec0g  5922  freccl  5932  oacl  5979  omcl  5980  oeicl  5981  addclpi  6311  mulclpi  6312  addclnq  6359  mulclnq  6360  addclnq0  6434  mulclnq0  6435  nqpnq0nq  6436  elnp1st2nd  6459  prarloclemcalc  6485  distrlem1prl  6558  distrlem1pru  6559  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemfl  6583  ltexprlemrl  6584  ltexprlemfu  6585  ltexprlemru  6586  addcanprlemu  6589  recexprlemloc  6603  aptiprleml  6611  addclsr  6681  mulclsr  6682  recexgt0sr  6701  mulextsr1lem  6706  axaddcl  6750  axaddrcl  6751  axmulcl  6752  axmulrcl  6753  subcl  7007  cru  7386  divclap  7439  redivclap  7489  cju  7694  nn1m1nn  7713  nnsub  7733  nnnn0addcl  7988  un0addcl  7991  peano2z  8057  peano2zm  8059  zaddcllemneg  8060  zaddcl  8061  nnaddm1cl  8081  nn0n0n1ge2  8087  zdivadd  8105  zdivmul  8106  zneo  8115  peano5uzti  8122  qmulz  8334  qnegcl  8347  qapne  8350  qdivcl  8352  cnref1o  8357  xnegcl  8515  xltnegi  8518  iccf1o  8642  ige3m2fz  8683  ige2m1fz1  8741  frec2uzzd  8867  frec2uzuzd  8869  frecuzrdgrrn  8875  frecuzrdgcl  8880  frecuzrdgsuc  8882  fzofig  8889  iseqovex  8899  expivallem  8910  exp1  8915  expcl2lemap  8921  m1expcl2  8931  expaddzap  8953  sqcl  8969  nnsqcl  8976  qsqcl  8978  zesq  9020  cjth  9074  imval  9078  recl  9081  imcl  9082  crre  9085  remim  9088  reim0b  9090  nn0abscl  9229
  Copyright terms: Public domain W3C validator