ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqeltrd GIF 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 (𝜑𝐴 = 𝐵)
eqeltrd.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
eqeltrd (𝜑𝐴𝐶)

Proof of Theorem eqeltrd
StepHypRef Expression
1 eqeltrd.2 . 2 (𝜑𝐵𝐶)
2 eqeltrd.1 . . 3 (𝜑𝐴 = 𝐵)
32eleq1d 2153 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 165 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  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  3965  opexg  4029  tfisi  4375  imain  5061  fvmptd  5348  fvmptdf  5353  fvmptt  5357  dffo3  5409  resfunexg  5479  f1oiso2  5567  riota2df  5589  riota5f  5593  ovmpt2dxf  5727  ovmpt2df  5733  offval  5820  iunexg  5847  oprabexd  5855  fo1stresm  5889  fo2ndresm  5890  1stdm  5909  1stconst  5943  2ndconst  5944  cnvf1olem  5946  fo2ndf  5949  f1od2  5957  iunon  6003  tfrlemibacc  6045  tfrlemibfn  6047  tfr1onlembacc  6061  tfr1onlembfn  6063  tfrcllembacc  6074  tfrcllembfn  6076  tfrcl  6083  rdgon  6105  frec0g  6116  freccllem  6121  frecfcllem  6123  frecsuclem  6125  oacl  6175  omcl  6176  oeicl  6177  fidifsnen  6538  en2eqpr  6575  unfiin  6588  ssfirab  6593  fnfi  6596  relcnvfi  6600  supclti  6637  supubti  6638  suplubti  6639  supelti  6641  ordiso2  6672  djulclr  6685  djurclr  6686  djulcl  6687  djurcl  6688  djuss  6705  updjudhcoinlf  6715  updjudhcoinrg  6716  cardcl  6753  addclpi  6830  mulclpi  6831  addclnq  6878  mulclnq  6879  addclnq0  6954  mulclnq0  6955  nqpnq0nq  6956  elnp1st2nd  6979  prarloclemcalc  7005  distrlem1prl  7085  distrlem1pru  7086  ltexprlemopl  7104  ltexprlemopu  7106  ltexprlemfl  7112  ltexprlemrl  7113  ltexprlemfu  7114  ltexprlemru  7115  addcanprlemu  7118  recexprlemloc  7134  aptiprleml  7142  caucvgprprlemopl  7200  addclsr  7243  mulclsr  7244  recexgt0sr  7263  mulextsr1lem  7269  axaddcl  7345  axaddrcl  7346  axmulcl  7347  axmulrcl  7348  axcaucvglemval  7376  subcl  7625  cru  8020  divclap  8084  redivclap  8137  lbinfcl  8345  cju  8356  nn1m1nn  8375  nnsub  8395  nnnn0addcl  8636  un0addcl  8639  peano2z  8719  peano2zm  8721  zaddcllemneg  8722  zaddcl  8723  nnaddm1cl  8744  nn0n0n1ge2  8750  zdivadd  8768  zdivmul  8769  suprzclex  8777  zneo  8780  peano5uzti  8787  supinfneg  9015  infsupneg  9016  qmulz  9040  qnegcl  9053  qapne  9056  qdivcl  9060  cnref1o  9065  xnegcl  9226  xltnegi  9229  iccf1o  9353  ige3m2fz  9395  ige2m1fz1  9453  rebtwn2z  9594  flqcl  9608  flapcl  9610  ceilqcl  9643  intfracq  9655  modqcl  9661  mulqmod0  9665  modqdifz  9671  zmodcl  9679  modfzo0difsn  9730  modsumfzodifsn  9731  frec2uzzd  9735  frec2uzsucd  9736  frec2uzuzd  9737  frecuzrdgrrn  9743  frec2uzrdg  9744  frecuzrdgrcl  9745  frecuzrdgsuc  9749  frecuzrdgrclt  9750  frecuzrdgg  9751  frecuzrdgsuctlem  9758  fzofig  9767  iseqovex  9787  iseqvalt  9790  iseqfclt  9794  iseqclt  9798  iseqcaopr3  9815  iseqf1olemnab  9822  iseqf1olemqk  9828  iseqf1olemjpcl  9829  iseqf1olemqpcl  9830  iseqf1olemfvp  9831  iseqf1olemqsumkj  9832  iseqf1olemqsum  9834  iseqf1oleml  9837  iseqf1o  9838  iser0f  9849  serile  9852  expivallem  9855  exp1  9860  expcl2lemap  9866  m1expcl2  9876  expaddzap  9898  sqcl  9915  nnsqcl  9923  qsqcl  9925  zesq  9969  facp1  10035  faccl  10040  facdiv  10043  bcval  10054  bcrpcl  10058  bcp1n  10066  bcpasc  10071  permnn  10076  hashennn  10085  hashcl  10086  shftlem  10147  ovshftex  10150  shftf  10161  cjth  10176  imval  10180  recl  10183  imcl  10184  crre  10187  remim  10190  reim0b  10192  cvg1nlemcau  10313  uzin2  10316  resqrexlem1arp  10334  resqrexlemp1rp  10335  resqrexlemglsq  10351  resqrexlemga  10352  resqrtcl  10358  abscl  10380  absrpclap  10390  nn0abscl  10414  fzomaxdiflem  10441  fzomaxdif  10442  maxabslemab  10535  maxcl  10539  zmaxcl  10552  minmax  10556  climaddc1  10611  climmulc2  10613  climsubc1  10614  climsubc2  10615  climle  10616  iisermulc2  10622  climlec2  10623  climcvg1nlem  10630  isumrblem  10657  fisumcvg  10658  isummolem3  10661  isummolem2a  10662  zisum  10665  fisum  10667  isumss  10671  fisumss  10672  isumss2  10673  fisumcvg2  10674  fsumcl2lem  10677  dvdsval2  10681  sqoddm1div8z  10768  zssinfcl  10826  infssuzex  10827  infssuzcldc  10829  gcdval  10833  gcdn0cl  10836  gcddvds  10837  divgcdnnr  10849  nn0seqcvgd  10905  ialgrlem1st  10906  ialgrlemconst  10907  ialgrp1  10910  eucalgf  10919  eucalglt  10921  lcmval  10927  lcmcllem  10931  lcmgcdlem  10941  cncongr2  10968  sqrt2irrlem  11022  oddpwdclemxy  11029  oddpwdclemdc  11033  qden1elz  11065  phicl2  11072  phimullem  11083  djucllem  11145  nnpredcl  11335  nninfsellemeq  11351  qdencn  11360
  Copyright terms: Public domain W3C validator