ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqeltrd Structured version   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  6433  mulclnq0  6434  nqpnq0nq  6435  elnp1st2nd  6458  prarloclemcalc  6484  distrlem1prl  6556  distrlem1pru  6557  ltexprlemopl  6573  ltexprlemopu  6575  ltexprlemfl  6581  ltexprlemrl  6582  ltexprlemfu  6583  ltexprlemru  6584  addcanprlemu  6587  recexprlemloc  6601  aptiprleml  6609  addclsr  6641  mulclsr  6642  recexgt0sr  6661  mulextsr1lem  6666  axaddcl  6710  axaddrcl  6711  axmulcl  6712  axmulrcl  6713  subcl  6967  cru  7346  divclap  7399  redivclap  7449  cju  7654  nn1m1nn  7673  nnsub  7693  nnnn0addcl  7948  un0addcl  7951  peano2z  8017  peano2zm  8019  zaddcllemneg  8020  zaddcl  8021  nnaddm1cl  8041  nn0n0n1ge2  8047  zdivadd  8065  zdivmul  8066  zneo  8075  peano5uzti  8082  qmulz  8294  qnegcl  8307  qapne  8310  qdivcl  8312  cnref1o  8317  xnegcl  8475  xltnegi  8478  iccf1o  8602  ige3m2fz  8643  ige2m1fz1  8701  frec2uzzd  8827  frec2uzuzd  8829  frecuzrdgrrn  8835  frecuzrdgcl  8840  frecuzrdgsuc  8842  fzofig  8849  iseqovex  8859  expivallem  8870  exp1  8875  expcl2lemap  8881  m1expcl2  8891  expaddzap  8913  sqcl  8929  nnsqcl  8936  qsqcl  8938  zesq  8980  cjth  9034  imval  9038  recl  9041  imcl  9042  crre  9045  remim  9048  reim0b  9050
  Copyright terms: Public domain W3C validator