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

Proof of Theorem eqeltrd
StepHypRef Expression
1 eqeltrd.2 . 2 (𝜑𝐵𝐶)
2 eqeltrd.1 . . 3 (𝜑𝐴 = 𝐵)
32eleq1d 2106 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 156 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243  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  3358  intab  3644  iinexgm  3908  opexg  3964  opexgOLD  3965  tfisi  4310  imain  4981  fvmptd  5253  fvmptdf  5258  fvmptt  5262  dffo3  5314  resfunexg  5382  f1oiso2  5466  riota2df  5488  riota5f  5492  ovmpt2dxf  5626  ovmpt2df  5632  offval  5719  iunexg  5746  oprabexd  5754  fo1stresm  5788  fo2ndresm  5789  1stdm  5808  1stconst  5842  2ndconst  5843  cnvf1olem  5845  fo2ndf  5848  iunon  5899  tfrlemibacc  5940  tfrlemibfn  5942  frec0g  5983  freccl  5993  oacl  6040  omcl  6041  oeicl  6042  fidifsnen  6331  ordiso2  6355  cardcl  6359  addclpi  6423  mulclpi  6424  addclnq  6471  mulclnq  6472  addclnq0  6547  mulclnq0  6548  nqpnq0nq  6549  elnp1st2nd  6572  prarloclemcalc  6598  distrlem1prl  6678  distrlem1pru  6679  ltexprlemopl  6697  ltexprlemopu  6699  ltexprlemfl  6705  ltexprlemrl  6706  ltexprlemfu  6707  ltexprlemru  6708  addcanprlemu  6711  recexprlemloc  6727  aptiprleml  6735  caucvgprprlemopl  6793  addclsr  6836  mulclsr  6837  recexgt0sr  6856  mulextsr1lem  6862  axaddcl  6938  axaddrcl  6939  axmulcl  6940  axmulrcl  6941  axcaucvglemval  6969  subcl  7208  cru  7591  divclap  7655  redivclap  7705  cju  7911  nn1m1nn  7930  nnsub  7950  nnnn0addcl  8210  un0addcl  8213  peano2z  8279  peano2zm  8281  zaddcllemneg  8282  zaddcl  8283  nnaddm1cl  8303  nn0n0n1ge2  8309  zdivadd  8327  zdivmul  8328  zneo  8337  peano5uzti  8344  qmulz  8556  qnegcl  8569  qapne  8572  qdivcl  8575  cnref1o  8580  xnegcl  8743  xltnegi  8746  iccf1o  8870  ige3m2fz  8911  ige2m1fz1  8969  rebtwn2z  9107  flqcl  9115  ceilqcl  9148  frec2uzzd  9160  frec2uzuzd  9162  frecuzrdgrrn  9168  frecuzrdgcl  9173  frecuzrdgsuc  9175  fzofig  9182  iseqovex  9193  iseqcaopr3  9214  iser0f  9225  serile  9227  expivallem  9230  exp1  9235  expcl2lemap  9241  m1expcl2  9251  expaddzap  9273  sqcl  9289  nnsqcl  9297  qsqcl  9299  zesq  9341  shftlem  9391  ovshftex  9394  shftf  9405  cjth  9420  imval  9424  recl  9427  imcl  9428  crre  9431  remim  9434  reim0b  9436  cvg1nlemcau  9557  uzin2  9560  resqrexlem1arp  9577  resqrexlemp1rp  9578  resqrexlemglsq  9594  resqrexlemga  9595  resqrtcl  9601  abscl  9623  absrpclap  9633  nn0abscl  9655  fzomaxdiflem  9682  fzomaxdif  9683  climaddc1  9823  climmulc2  9825  climsubc1  9826  climsubc2  9827  climle  9828  iisermulc2  9834  climlec2  9835  climcvg1nlem  9842  sqr2irrlem  9851  nn0seqcvgd  9854  ialgrlem1st  9855  ialgrlemconst  9856  ialgrp1  9859  qdencn  10097
  Copyright terms: Public domain W3C validator