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

Theorem eqeltrd 2096
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 2088 . 2 (φ → (A 𝐶B 𝐶))
41, 3mpbird 156 1 (φA 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1228   wcel 1374
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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015  df-clel 2018
This theorem is referenced by:  eqeltrrd  2097  3eltr4d  2103  syl5eqel  2106  syl6eqel  2110  intab  3618  iinexgm  3882  opexg  3938  opexgOLD  3939  tfisi  4237  imain  4907  fvmptd  5178  fvmptdf  5183  fvmptt  5187  dffo3  5239  resfunexg  5307  f1oiso2  5391  riota2df  5412  riota5f  5416  ovmpt2dxf  5549  ovmpt2df  5555  offval  5642  iunexg  5669  oprabexd  5677  fo1stresm  5711  fo2ndresm  5712  1stdm  5731  1stconst  5765  2ndconst  5766  cnvf1olem  5768  fo2ndf  5771  iunon  5821  tfrlemibacc  5861  tfrlemibfn  5863  oacl  5955  omcl  5956  oeicl  5957  addclpi  6187  mulclpi  6188  addclnq  6234  mulclnq  6235  addclnq0  6306  mulclnq0  6307  nqpnq0nq  6308  elnp1st2nd  6330  prarloclemcalc  6356  distrlem1prl  6421  distrlem1pru  6422  ltexprlemopl  6438  ltexprlemopu  6440  ltexprlemfl  6446  ltexprlemrl  6447  ltexprlemfu  6448  ltexprlemru  6449  addcanprlemu  6452  recexprlemloc  6465  addclsr  6500  mulclsr  6501  recexsrlem  6520  axaddcl  6560  axaddrcl  6561  axmulcl  6562  axmulrcl  6563  subcl  6797
  Copyright terms: Public domain W3C validator