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  6557  distrlem1pru  6558  ltexprlemopl  6574  ltexprlemopu  6576  ltexprlemfl  6582  ltexprlemrl  6583  ltexprlemfu  6584  ltexprlemru  6585  addcanprlemu  6588  recexprlemloc  6602  aptiprleml  6610  addclsr  6661  mulclsr  6662  recexgt0sr  6681  mulextsr1lem  6686  axaddcl  6730  axaddrcl  6731  axmulcl  6732  axmulrcl  6733  subcl  6987  cru  7366  divclap  7419  redivclap  7469  cju  7674  nn1m1nn  7693  nnsub  7713  nnnn0addcl  7968  un0addcl  7971  peano2z  8037  peano2zm  8039  zaddcllemneg  8040  zaddcl  8041  nnaddm1cl  8061  nn0n0n1ge2  8067  zdivadd  8085  zdivmul  8086  zneo  8095  peano5uzti  8102  qmulz  8314  qnegcl  8327  qapne  8330  qdivcl  8332  cnref1o  8337  xnegcl  8495  xltnegi  8498  iccf1o  8622  ige3m2fz  8663  ige2m1fz1  8721  frec2uzzd  8847  frec2uzuzd  8849  frecuzrdgrrn  8855  frecuzrdgcl  8860  frecuzrdgsuc  8862  fzofig  8869  iseqovex  8879  expivallem  8890  exp1  8895  expcl2lemap  8901  m1expcl2  8911  expaddzap  8933  sqcl  8949  nnsqcl  8956  qsqcl  8958  zesq  9000  cjth  9054  imval  9058  recl  9061  imcl  9062  crre  9065  remim  9068  reim0b  9070  nn0abscl  9209
  Copyright terms: Public domain W3C validator