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

Theorem eqeltrd 2165
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 2157 . 2  |-  ( ph  ->  ( A  e.  C  <->  B  e.  C ) )
41, 3mpbird 166 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1290    e. wcel 1439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-ext 2071
This theorem depends on definitions:  df-bi 116  df-cleq 2082  df-clel 2085
This theorem is referenced by:  eqeltrrd  2166  3eltr4d  2172  syl5eqel  2175  syl6eqel  2179  ifcldadc  3424  ifcldcd  3430  intab  3723  disjiun  3846  iinexgm  3996  opexg  4064  tfisi  4415  nnpredcl  4449  imain  5109  fvmptd  5398  fvmptdf  5403  fvmptt  5407  dffo3  5460  resfunexg  5532  f1oiso2  5620  riota2df  5642  riota5f  5646  ovmpt2dxf  5784  ovmpt2df  5790  offval  5877  iunexg  5904  oprabexd  5912  fo1stresm  5946  fo2ndresm  5947  1stdm  5966  1stconst  6000  2ndconst  6001  cnvf1olem  6003  fo2ndf  6006  f1od2  6014  iunon  6063  tfrlemibacc  6105  tfrlemibfn  6107  tfr1onlembacc  6121  tfr1onlembfn  6123  tfrcllembacc  6134  tfrcllembfn  6136  tfrcl  6143  rdgon  6165  frec0g  6176  freccllem  6181  frecfcllem  6183  frecsuclem  6185  oacl  6235  omcl  6236  oeicl  6237  mptelixpg  6505  fidifsnen  6640  en2eqpr  6677  unfiin  6690  ssfirab  6697  fnfi  6700  relcnvfi  6704  fidcenumlemr  6718  supclti  6747  supubti  6748  suplubti  6749  supelti  6751  ordiso2  6782  djulclr  6795  djurclr  6796  djulcl  6797  djurcl  6798  djuss  6815  updjudhcoinlf  6825  updjudhcoinrg  6826  enumctlemm  6846  cardcl  6870  addclpi  6947  mulclpi  6948  addclnq  6995  mulclnq  6996  addclnq0  7071  mulclnq0  7072  nqpnq0nq  7073  elnp1st2nd  7096  prarloclemcalc  7122  distrlem1prl  7202  distrlem1pru  7203  ltexprlemopl  7221  ltexprlemopu  7223  ltexprlemfl  7229  ltexprlemrl  7230  ltexprlemfu  7231  ltexprlemru  7232  addcanprlemu  7235  recexprlemloc  7251  aptiprleml  7259  caucvgprprlemopl  7317  addclsr  7360  mulclsr  7361  recexgt0sr  7380  mulextsr1lem  7386  axaddcl  7462  axaddrcl  7463  axmulcl  7464  axmulrcl  7465  axcaucvglemval  7493  subcl  7742  cru  8140  divclap  8206  redivclap  8259  lbinfcl  8471  cju  8482  nn1m1nn  8501  nnsub  8522  nnnn0addcl  8764  un0addcl  8767  peano2z  8847  peano2zm  8849  zaddcllemneg  8850  zaddcl  8851  nnaddm1cl  8872  nn0n0n1ge2  8878  zdivadd  8896  zdivmul  8897  suprzclex  8905  zneo  8908  peano5uzti  8915  supinfneg  9144  infsupneg  9145  qmulz  9169  qnegcl  9182  qapne  9185  qdivcl  9189  cnref1o  9194  xnegcl  9355  xltnegi  9358  iccf1o  9482  ige3m2fz  9524  ige2m1fz1  9584  rebtwn2z  9727  flqcl  9741  flapcl  9743  ceilqcl  9776  intfracq  9788  modqcl  9794  mulqmod0  9798  modqdifz  9804  zmodcl  9812  modfzo0difsn  9863  modsumfzodifsn  9864  frec2uzzd  9868  frec2uzsucd  9869  frec2uzuzd  9870  frecuzrdgrrn  9876  frec2uzrdg  9877  frecuzrdgrcl  9878  frecuzrdgsuc  9882  frecuzrdgrclt  9883  frecuzrdgg  9884  frecuzrdgsuctlem  9891  fzofig  9900  iseqovex  9931  iseqvalt  9934  seq3val  9935  iseqfclt  9940  seqf  9941  seq3clss  9948  iseqcaopr3  9971  iseqf1olemnab  9978  iseqf1olemqk  9984  iseqf1olemjpcl  9985  iseqf1olemqpcl  9986  iseqf1olemfvp  9987  seq3f1olemqsumkj  9988  seq3f1olemqsum  9990  seq3f1oleml  9993  seq3f1o  9994  ser3add  9996  seq3distr  10007  iser0f  10009  ser0f  10011  ser3le  10014  exp3vallem  10017  exp3val  10018  exp1  10022  expcl2lemap  10028  m1expcl2  10038  expaddzap  10060  sqcl  10077  nnsqcl  10085  qsqcl  10087  zesq  10133  facp1  10199  faccl  10204  facdiv  10207  bcval  10218  bcrpcl  10222  bcp1n  10230  bcpasc  10235  permnn  10240  hashennn  10249  hashcl  10250  shftlem  10311  ovshftex  10314  shftf  10325  seq3shft  10333  cjth  10341  imval  10345  recl  10348  imcl  10349  crre  10352  remim  10355  reim0b  10357  cvg1nlemcau  10478  uzin2  10481  resqrexlem1arp  10499  resqrexlemp1rp  10500  resqrexlemglsq  10516  resqrexlemga  10517  resqrtcl  10523  abscl  10545  absrpclap  10555  nn0abscl  10579  fzomaxdiflem  10606  fzomaxdif  10607  maxabslemab  10700  maxcl  10704  zmaxcl  10717  minmax  10722  climaddc1  10778  climmulc2  10780  climsubc1  10781  climsubc2  10782  climle  10783  iisermulc2  10789  isermulc2  10790  climlec2  10791  climcvg1nlem  10799  isumrblem  10826  fisumcvg  10827  fsum3cvg  10828  isummolem3  10831  isummolem2a  10832  zisum  10835  isum  10837  fsumgcl  10838  fisum  10839  fsum3  10840  isumss  10844  fisumss  10845  isumss2  10846  fisumcvg2  10847  fsum3cvg2  10848  fisumser  10851  fsum3ser  10852  fsumcl2lem  10853  fsumcllem  10854  fsumadd  10861  sumsnf  10864  fsumsplitsn  10865  isumclim  10876  isumcl  10880  isummulc2  10881  isumrecl  10884  isumge0  10885  isumadd  10886  fsum2dlemstep  10889  fisumcom2  10893  mptfzshft  10897  fsumrev  10898  fsummulc2  10903  iserabs  10930  isumshft  10945  isumsplit  10946  isum1p  10947  isumrpcl  10949  isumle  10950  isumlessdc  10951  trireciplem  10955  expcnvap0  10957  expcnvre  10958  expcnv  10959  explecnv  10960  geolim  10966  geolim2  10967  geo2lim  10971  cvgratnnlemsumlt  10983  cvgratz  10987  mertenslemub  10989  mertenslemi1  10990  mertenslem2  10991  mertensabs  10992  efcllemp  11009  ef0lem  11011  efcvgfsum  11018  reefcl  11019  ege2le3  11022  efcj  11024  efaddlem  11025  eftlcvg  11038  eftlcl  11039  reeftlcl  11040  eftlub  11041  efsep  11042  effsumlt  11043  efgt1p2  11046  efgt1p  11047  reeff1  11052  tanclap  11061  resincl  11072  recoscl  11073  retanclap  11074  eirraplem  11125  dvdsval2  11138  sqoddm1div8z  11225  zssinfcl  11283  infssuzex  11284  infssuzcldc  11286  gcdval  11290  gcdn0cl  11293  gcddvds  11294  divgcdnnr  11306  nn0seqcvgd  11362  ialgrlem1st  11363  ialgrlemconst  11364  algrf  11366  algrp1  11367  eucalgf  11376  eucalglt  11378  lcmval  11384  lcmcllem  11388  lcmgcdlem  11398  cncongr2  11425  sqrt2irrlem  11479  oddpwdclemxy  11486  oddpwdclemdc  11490  qden1elz  11522  phicl2  11529  phimullem  11540  setsex  11587  strsetsid  11588  ressid2  11614  ressval2  11615  ressid  11616  iunopn  11762  toponmax  11784  tgvalex  11811  tgtop  11829  tgiun  11834  tgidm  11835  ntropn  11878  cncfval  11901  divccncfap  11919  djucllem  11973  nninfsellemeq  12178  qdencn  12187
  Copyright terms: Public domain W3C validator