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  6416  nqnq0  6423  addcmpblnq0  6425  mulcmpblnq0  6426  mulcanenq0ec  6427  addclnq0  6433  mulclnq0  6434  nqpnq0nq  6435  nq0m0r  6438  distrnq0  6441  addassnq0lemcl  6443  prarloclemlt  6475  prarloclem5  6482  distrlem4prl  6558  distrlem4pru  6559  ltexprlemm  6572  ltexprlemrl  6582  ltexprlemru  6584  addcanprleml  6586  prsrlem1  6630  mulgt0sr  6664  cnegexlem2  6944  subf  6970  resubcl  7031  negcon1ad  7073  subeq0bd  7133  rimul  7329  rereim  7330  nn0nnaddcl  7949  elnn0nn  7960  zaddcllemneg  8020  zsubcl  8022  zrevaddcl  8031  elz2  8048  zdiv  8064  peano5uzti  8082  peano2uzr  8264  uzaddcl  8265  divfnzn  8292  qsubcl  8309  qrevaddcl  8313  fseq1p1m1  8686  frec2uzrand  8832  frecuzrdglem  8838  frecuzrdg0  8841  expaddzaplem  8912  expaddzap  8913  expmulzap  8915  zesq  8980  ref  9043  imf  9044  crre  9045  rereb  9051
  Copyright terms: Public domain W3C validator