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

Theorem eqeltrrd 2112
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eqeltrrd.1 (φA = B)
eqeltrrd.2 (φA 𝐶)
Assertion
Ref Expression
eqeltrrd (φB 𝐶)

Proof of Theorem eqeltrrd
StepHypRef Expression
1 eqeltrrd.1 . . 3 (φA = B)
21eqcomd 2042 . 2 (φB = A)
3 eqeltrrd.2 . 2 (φA 𝐶)
42, 3eqeltrd 2111 1 (φB 𝐶)
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:  3eltr3d  2117  xpexr2m  4705  funimaexg  4926  fvmptdv2  5203  ffvresb  5271  2ndrn  5751  1st2ndbr  5752  elopabi  5763  cnvf1olem  5787  dftpos4  5819  tfrlemibxssdm  5882  nnmordi  6025  th3qlem1  6144  archnqq  6400  prarloclemarch2  6402  enq0tr  6417  nqnq0  6424  addcmpblnq0  6426  mulcmpblnq0  6427  mulcanenq0ec  6428  addclnq0  6434  mulclnq0  6435  nqpnq0nq  6436  nq0m0r  6439  distrnq0  6442  addassnq0lemcl  6444  prarloclemlt  6476  prarloclem5  6483  distrlem4prl  6560  distrlem4pru  6561  ltexprlemm  6574  ltexprlemrl  6584  ltexprlemru  6586  addcanprleml  6588  cauappcvgprlemladdru  6628  prsrlem1  6670  mulgt0sr  6704  cnegexlem2  6984  subf  7010  resubcl  7071  negcon1ad  7113  subeq0bd  7173  rimul  7369  rereim  7370  nn0nnaddcl  7989  elnn0nn  8000  zaddcllemneg  8060  zsubcl  8062  zrevaddcl  8071  elz2  8088  zdiv  8104  peano5uzti  8122  peano2uzr  8304  uzaddcl  8305  divfnzn  8332  qsubcl  8349  qrevaddcl  8353  fseq1p1m1  8726  frec2uzrand  8872  frecuzrdglem  8878  frecuzrdg0  8881  expaddzaplem  8952  expaddzap  8953  expmulzap  8955  zesq  9020  ref  9083  imf  9084  crre  9085  rereb  9091
  Copyright terms: Public domain W3C validator