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

Theorem eqeltrd 2161
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 2153 . 2  |-  ( ph  ->  ( A  e.  C  <->  B  e.  C ) )
41, 3mpbird 165 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1287    e. wcel 1436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081
This theorem is referenced by:  eqeltrrd  2162  3eltr4d  2168  syl5eqel  2171  syl6eqel  2175  ifcldadc  3406  ifcldcd  3412  intab  3700  iinexgm  3964  opexg  4028  tfisi  4374  imain  5058  fvmptd  5342  fvmptdf  5347  fvmptt  5351  dffo3  5403  resfunexg  5473  f1oiso2  5561  riota2df  5583  riota5f  5587  ovmpt2dxf  5721  ovmpt2df  5727  offval  5814  iunexg  5841  oprabexd  5849  fo1stresm  5883  fo2ndresm  5884  1stdm  5903  1stconst  5937  2ndconst  5938  cnvf1olem  5940  fo2ndf  5943  f1od2  5951  iunon  5997  tfrlemibacc  6039  tfrlemibfn  6041  tfr1onlembacc  6055  tfr1onlembfn  6057  tfrcllembacc  6068  tfrcllembfn  6070  tfrcl  6077  rdgon  6099  frec0g  6110  freccllem  6115  frecfcllem  6117  frecsuclem  6119  oacl  6169  omcl  6170  oeicl  6171  fidifsnen  6532  en2eqpr  6569  unfiin  6582  ssfirab  6587  fnfi  6590  relcnvfi  6594  supclti  6630  supubti  6631  suplubti  6632  supelti  6634  ordiso2  6665  djulclr  6678  djurclr  6679  djulcl  6680  djurcl  6681  djuss  6698  updjudhcoinlf  6708  updjudhcoinrg  6709  cardcl  6746  addclpi  6823  mulclpi  6824  addclnq  6871  mulclnq  6872  addclnq0  6947  mulclnq0  6948  nqpnq0nq  6949  elnp1st2nd  6972  prarloclemcalc  6998  distrlem1prl  7078  distrlem1pru  7079  ltexprlemopl  7097  ltexprlemopu  7099  ltexprlemfl  7105  ltexprlemrl  7106  ltexprlemfu  7107  ltexprlemru  7108  addcanprlemu  7111  recexprlemloc  7127  aptiprleml  7135  caucvgprprlemopl  7193  addclsr  7236  mulclsr  7237  recexgt0sr  7256  mulextsr1lem  7262  axaddcl  7338  axaddrcl  7339  axmulcl  7340  axmulrcl  7341  axcaucvglemval  7369  subcl  7618  cru  8013  divclap  8077  redivclap  8130  lbinfcl  8338  cju  8349  nn1m1nn  8368  nnsub  8388  nnnn0addcl  8629  un0addcl  8632  peano2z  8712  peano2zm  8714  zaddcllemneg  8715  zaddcl  8716  nnaddm1cl  8737  nn0n0n1ge2  8743  zdivadd  8761  zdivmul  8762  suprzclex  8770  zneo  8773  peano5uzti  8780  supinfneg  9008  infsupneg  9009  qmulz  9033  qnegcl  9046  qapne  9049  qdivcl  9053  cnref1o  9058  xnegcl  9219  xltnegi  9222  iccf1o  9346  ige3m2fz  9388  ige2m1fz1  9446  rebtwn2z  9587  flqcl  9601  flapcl  9603  ceilqcl  9636  intfracq  9648  modqcl  9654  mulqmod0  9658  modqdifz  9664  zmodcl  9672  modfzo0difsn  9723  modsumfzodifsn  9724  frec2uzzd  9728  frec2uzsucd  9729  frec2uzuzd  9730  frecuzrdgrrn  9736  frec2uzrdg  9737  frecuzrdgrcl  9738  frecuzrdgsuc  9742  frecuzrdgrclt  9743  frecuzrdgg  9744  frecuzrdgsuctlem  9751  fzofig  9760  iseqovex  9780  iseqvalt  9783  iseqfclt  9787  iseqcaopr3  9807  iseqf1olemnab  9814  iseqf1olemqk  9820  iseqf1olemjpcl  9821  iseqf1olemqpcl  9822  iseqf1olemfvp  9823  iseqf1olemqsumkj  9824  iseqf1olemqsum  9826  iseqf1oleml  9829  iseqf1o  9830  iser0f  9841  serile  9844  expivallem  9847  exp1  9852  expcl2lemap  9858  m1expcl2  9868  expaddzap  9890  sqcl  9907  nnsqcl  9915  qsqcl  9917  zesq  9961  facp1  10027  faccl  10032  facdiv  10035  bcval  10046  bcrpcl  10050  bcp1n  10058  bcpasc  10063  permnn  10068  hashennn  10077  hashcl  10078  shftlem  10139  ovshftex  10142  shftf  10153  cjth  10168  imval  10172  recl  10175  imcl  10176  crre  10179  remim  10182  reim0b  10184  cvg1nlemcau  10305  uzin2  10308  resqrexlem1arp  10326  resqrexlemp1rp  10327  resqrexlemglsq  10343  resqrexlemga  10344  resqrtcl  10350  abscl  10372  absrpclap  10382  nn0abscl  10406  fzomaxdiflem  10433  fzomaxdif  10434  maxabslemab  10527  maxcl  10531  minmax  10547  climaddc1  10602  climmulc2  10604  climsubc1  10605  climsubc2  10606  climle  10607  iisermulc2  10613  climlec2  10614  climcvg1nlem  10621  isumrblem  10648  fisumcvg  10649  isummolem3  10652  isummolem2a  10653  zisum  10656  fisum  10658  isumss  10662  dvdsval2  10666  sqoddm1div8z  10753  zssinfcl  10811  infssuzex  10812  infssuzcldc  10814  gcdval  10818  gcdn0cl  10821  gcddvds  10822  divgcdnnr  10834  nn0seqcvgd  10890  ialgrlem1st  10891  ialgrlemconst  10892  ialgrp1  10895  eucalgf  10904  eucalglt  10906  lcmval  10912  lcmcllem  10916  lcmgcdlem  10926  cncongr2  10953  sqrt2irrlem  11007  oddpwdclemxy  11014  oddpwdclemdc  11018  qden1elz  11050  phicl2  11057  phimullem  11068  djucllem  11130  nnpredcl  11320  nninfsellemeq  11336  qdencn  11345
  Copyright terms: Public domain W3C validator