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

Theorem eqeltrd 2130
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 2122 . 2  |-  ( ph  ->  ( A  e.  C  <->  B  e.  C ) )
41, 3mpbird 160 1  |-  ( ph  ->  A  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:  eqeltrrd  2131  3eltr4d  2137  syl5eqel  2140  syl6eqel  2144  ifcldcd  3386  intab  3672  iinexgm  3936  opexg  3992  opexgOLD  3993  tfisi  4338  imain  5009  fvmptd  5281  fvmptdf  5286  fvmptt  5290  dffo3  5342  resfunexg  5410  f1oiso2  5494  riota2df  5516  riota5f  5520  ovmpt2dxf  5654  ovmpt2df  5660  offval  5747  iunexg  5774  oprabexd  5782  fo1stresm  5816  fo2ndresm  5817  1stdm  5836  1stconst  5870  2ndconst  5871  cnvf1olem  5873  fo2ndf  5876  f1od2  5884  iunon  5930  tfrlemibacc  5971  tfrlemibfn  5973  frec0g  6014  freccl  6024  oacl  6071  omcl  6072  oeicl  6073  fidifsnen  6362  supclti  6404  supubti  6405  suplubti  6406  ordiso2  6415  cardcl  6419  addclpi  6483  mulclpi  6484  addclnq  6531  mulclnq  6532  addclnq0  6607  mulclnq0  6608  nqpnq0nq  6609  elnp1st2nd  6632  prarloclemcalc  6658  distrlem1prl  6738  distrlem1pru  6739  ltexprlemopl  6757  ltexprlemopu  6759  ltexprlemfl  6765  ltexprlemrl  6766  ltexprlemfu  6767  ltexprlemru  6768  addcanprlemu  6771  recexprlemloc  6787  aptiprleml  6795  caucvgprprlemopl  6853  addclsr  6896  mulclsr  6897  recexgt0sr  6916  mulextsr1lem  6922  axaddcl  6998  axaddrcl  6999  axmulcl  7000  axmulrcl  7001  axcaucvglemval  7029  subcl  7273  cru  7667  divclap  7731  redivclap  7782  cju  7989  nn1m1nn  8008  nnsub  8028  nnnn0addcl  8269  un0addcl  8272  peano2z  8338  peano2zm  8340  zaddcllemneg  8341  zaddcl  8342  nnaddm1cl  8363  nn0n0n1ge2  8369  zdivadd  8387  zdivmul  8388  zneo  8398  peano5uzti  8405  qmulz  8655  qnegcl  8668  qapne  8671  qdivcl  8675  cnref1o  8680  xnegcl  8846  xltnegi  8849  iccf1o  8973  ige3m2fz  9015  ige2m1fz1  9073  rebtwn2z  9211  flqcl  9225  ceilqcl  9258  intfracq  9270  modqcl  9276  mulqmod0  9280  modqdifz  9286  zmodcl  9294  modfzo0difsn  9345  modsumfzodifsn  9346  frec2uzzd  9350  frec2uzuzd  9352  frecuzrdgrrn  9358  frecuzrdgcl  9363  frecuzrdgsuc  9365  fzofig  9372  iseqovex  9383  iseqcaopr3  9404  iser0f  9416  serile  9418  expivallem  9421  exp1  9426  expcl2lemap  9432  m1expcl2  9442  expaddzap  9464  sqcl  9481  nnsqcl  9489  qsqcl  9491  zesq  9535  facp1  9598  faccl  9603  facdiv  9606  bcval  9617  bcrpcl  9621  bcp1n  9629  bcpasc  9634  permnn  9639  shftlem  9645  ovshftex  9648  shftf  9659  cjth  9674  imval  9678  recl  9681  imcl  9682  crre  9685  remim  9688  reim0b  9690  cvg1nlemcau  9811  uzin2  9814  resqrexlem1arp  9832  resqrexlemp1rp  9833  resqrexlemglsq  9849  resqrexlemga  9850  resqrtcl  9856  abscl  9878  absrpclap  9888  nn0abscl  9912  fzomaxdiflem  9939  fzomaxdif  9940  climaddc1  10080  climmulc2  10082  climsubc1  10083  climsubc2  10084  climle  10085  iisermulc2  10091  climlec2  10092  climcvg1nlem  10099  dvdsval2  10111  sqoddm1div8z  10198  sqr2irrlem  10250  oddpwdclemxy  10257  oddpwdclemdc  10261  nn0seqcvgd  10263  ialgrlem1st  10264  ialgrlemconst  10265  ialgrp1  10268  qdencn  10511
  Copyright terms: Public domain W3C validator