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

Theorem eqeltrd 2114
Description: Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
Hypotheses
Ref Expression
eqeltrd.1  |-  ( ph  ->  A  =  B )
eqeltrd.2  |-  ( ph  ->  B  e.  C )
Assertion
Ref Expression
eqeltrd  |-  ( ph  ->  A  e.  C )

Proof of Theorem eqeltrd
StepHypRef Expression
1 eqeltrd.2 . 2  |-  ( ph  ->  B  e.  C )
2 eqeltrd.1 . . 3  |-  ( ph  ->  A  =  B )
32eleq1d 2106 . 2  |-  ( ph  ->  ( A  e.  C  <->  B  e.  C ) )
41, 3mpbird 156 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1243    e. wcel 1393
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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036
This theorem is referenced by:  eqeltrrd  2115  3eltr4d  2121  syl5eqel  2124  syl6eqel  2128  ifcldcd  3355  intab  3641  iinexgm  3905  opexg  3961  opexgOLD  3962  tfisi  4288  imain  4959  fvmptd  5231  fvmptdf  5236  fvmptt  5240  dffo3  5292  resfunexg  5360  f1oiso2  5444  riota2df  5466  riota5f  5470  ovmpt2dxf  5604  ovmpt2df  5610  offval  5697  iunexg  5724  oprabexd  5732  fo1stresm  5766  fo2ndresm  5767  1stdm  5786  1stconst  5820  2ndconst  5821  cnvf1olem  5823  fo2ndf  5826  iunon  5877  tfrlemibacc  5918  tfrlemibfn  5920  frec0g  5961  freccl  5971  oacl  6018  omcl  6019  oeicl  6020  fidifsnen  6309  cardcl  6333  addclpi  6397  mulclpi  6398  addclnq  6445  mulclnq  6446  addclnq0  6521  mulclnq0  6522  nqpnq0nq  6523  elnp1st2nd  6546  prarloclemcalc  6572  distrlem1prl  6652  distrlem1pru  6653  ltexprlemopl  6671  ltexprlemopu  6673  ltexprlemfl  6679  ltexprlemrl  6680  ltexprlemfu  6681  ltexprlemru  6682  addcanprlemu  6685  recexprlemloc  6701  aptiprleml  6709  caucvgprprlemopl  6767  addclsr  6810  mulclsr  6811  recexgt0sr  6830  mulextsr1lem  6836  axaddcl  6912  axaddrcl  6913  axmulcl  6914  axmulrcl  6915  axcaucvglemval  6943  subcl  7181  cru  7560  divclap  7624  redivclap  7674  cju  7880  nn1m1nn  7899  nnsub  7919  nnnn0addcl  8175  un0addcl  8178  peano2z  8244  peano2zm  8246  zaddcllemneg  8247  zaddcl  8248  nnaddm1cl  8268  nn0n0n1ge2  8274  zdivadd  8292  zdivmul  8293  zneo  8302  peano5uzti  8309  qmulz  8521  qnegcl  8534  qapne  8537  qdivcl  8539  cnref1o  8544  xnegcl  8703  xltnegi  8706  iccf1o  8830  ige3m2fz  8871  ige2m1fz1  8929  frec2uzzd  9055  frec2uzuzd  9057  frecuzrdgrrn  9063  frecuzrdgcl  9068  frecuzrdgsuc  9070  fzofig  9077  iseqovex  9088  iseqcaopr3  9109  iser0f  9120  serile  9122  expivallem  9125  exp1  9130  expcl2lemap  9136  m1expcl2  9146  expaddzap  9168  sqcl  9184  nnsqcl  9192  qsqcl  9194  zesq  9236  shftlem  9286  ovshftex  9289  shftf  9300  cjth  9315  imval  9319  recl  9322  imcl  9323  crre  9326  remim  9329  reim0b  9331  cvg1nlemcau  9452  uzin2  9455  resqrexlem1arp  9472  resqrexlemp1rp  9473  resqrexlemglsq  9489  resqrexlemga  9490  resqrtcl  9496  abscl  9518  absrpclap  9528  nn0abscl  9550  fzomaxdiflem  9577  fzomaxdif  9578  climaddc1  9717  climmulc2  9719  climsubc1  9720  climsubc2  9721  climle  9722  iisermulc2  9728  climlec2  9729  climcvg1nlem  9736  sqr2irrlem  9745  nn0seqcvgd  9748  ialgrlem1st  9749  ialgrlemconst  9750  ialgrp1  9753
  Copyright terms: Public domain W3C validator