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

Theorem eqeltrrd 2131
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eqeltrrd.1  |-  ( ph  ->  A  =  B )
eqeltrrd.2  |-  ( ph  ->  A  e.  C )
Assertion
Ref Expression
eqeltrrd  |-  ( ph  ->  B  e.  C )

Proof of Theorem eqeltrrd
StepHypRef Expression
1 eqeltrrd.1 . . 3  |-  ( ph  ->  A  =  B )
21eqcomd 2061 . 2  |-  ( ph  ->  B  =  A )
3 eqeltrrd.2 . 2  |-  ( ph  ->  A  e.  C )
42, 3eqeltrd 2130 1  |-  ( ph  ->  B  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259    e. wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  3eltr3d  2136  xpexr2m  4790  funimaexg  5011  fvmptdv2  5288  ffvresb  5356  2ndrn  5837  1st2ndbr  5838  elopabi  5849  cnvf1olem  5873  dftpos4  5909  tfrlemibxssdm  5972  nnmordi  6120  th3qlem1  6239  onunsnss  6386  ordiso2  6415  archnqq  6573  prarloclemarch2  6575  enq0tr  6590  nqnq0  6597  addcmpblnq0  6599  mulcmpblnq0  6600  mulcanenq0ec  6601  addclnq0  6607  mulclnq0  6608  nqpnq0nq  6609  nq0m0r  6612  distrnq0  6615  addassnq0lemcl  6617  prarloclemlt  6649  prarloclem5  6656  distrlem4prl  6740  distrlem4pru  6741  ltexprlemm  6756  ltexprlemrl  6766  ltexprlemru  6768  addcanprleml  6770  cauappcvgprlemladdru  6812  prsrlem1  6885  mulgt0sr  6920  cnegexlem2  7250  subf  7276  resubcl  7338  negcon1ad  7380  subeq0bd  7449  rimul  7650  rereim  7651  nn0nnaddcl  8270  elnn0nn  8281  zaddcllemneg  8341  zsubcl  8343  zrevaddcl  8352  elz2  8370  zdiv  8386  peano5uzti  8405  peano2uzr  8624  uzaddcl  8625  divfnzn  8653  qsubcl  8670  qrevaddcl  8676  fseq1p1m1  9058  modqmuladdim  9317  frec2uzrand  9355  frecuzrdglem  9361  frecuzrdg0  9364  iseqfeq  9395  iseqdistr  9414  serige0  9417  serile  9418  expaddzaplem  9463  expaddzap  9464  expmulzap  9466  zesq  9535  bcm1k  9628  bccl  9635  permnn  9639  shftuz  9646  ref  9683  imf  9684  crre  9685  rereb  9691  resqrexlemnm  9845  absf  9937  iserile  10093  oexpneg  10188  nn0ob  10220  divalglemqt  10231  sqr2irrlem  10250
  Copyright terms: Public domain W3C validator