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

Theorem eqeltrd 2156
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 2148 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 165 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285  wcel 1434
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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078
This theorem is referenced by:  eqeltrrd  2157  3eltr4d  2163  syl5eqel  2166  syl6eqel  2170  ifcldadc  3386  ifcldcd  3389  intab  3673  iinexgm  3937  opexg  3991  tfisi  4336  imain  5012  fvmptd  5285  fvmptdf  5290  fvmptt  5294  dffo3  5346  resfunexg  5414  f1oiso2  5497  riota2df  5519  riota5f  5523  ovmpt2dxf  5657  ovmpt2df  5663  offval  5750  iunexg  5777  oprabexd  5785  fo1stresm  5819  fo2ndresm  5820  1stdm  5839  1stconst  5873  2ndconst  5874  cnvf1olem  5876  fo2ndf  5879  f1od2  5887  iunon  5933  tfrlemibacc  5975  tfrlemibfn  5977  tfr1onlembacc  5991  tfr1onlembfn  5993  tfrcllembacc  6004  tfrcllembfn  6006  tfrcl  6013  rdgon  6035  frec0g  6046  freccllem  6051  frecfcllem  6053  frecsuclem  6055  oacl  6104  omcl  6105  oeicl  6106  fidifsnen  6405  en2eqpr  6434  unfiin  6444  fnfi  6446  relcnvfi  6449  supclti  6470  supubti  6471  suplubti  6472  supelti  6474  ordiso2  6505  cardcl  6509  addclpi  6579  mulclpi  6580  addclnq  6627  mulclnq  6628  addclnq0  6703  mulclnq0  6704  nqpnq0nq  6705  elnp1st2nd  6728  prarloclemcalc  6754  distrlem1prl  6834  distrlem1pru  6835  ltexprlemopl  6853  ltexprlemopu  6855  ltexprlemfl  6861  ltexprlemrl  6862  ltexprlemfu  6863  ltexprlemru  6864  addcanprlemu  6867  recexprlemloc  6883  aptiprleml  6891  caucvgprprlemopl  6949  addclsr  6992  mulclsr  6993  recexgt0sr  7012  mulextsr1lem  7018  axaddcl  7094  axaddrcl  7095  axmulcl  7096  axmulrcl  7097  axcaucvglemval  7125  subcl  7374  cru  7769  divclap  7833  redivclap  7886  lbinfcl  8094  cju  8105  nn1m1nn  8124  nnsub  8144  nnnn0addcl  8385  un0addcl  8388  peano2z  8468  peano2zm  8470  zaddcllemneg  8471  zaddcl  8472  nnaddm1cl  8493  nn0n0n1ge2  8499  zdivadd  8517  zdivmul  8518  suprzclex  8526  zneo  8529  peano5uzti  8536  supinfneg  8764  infsupneg  8765  qmulz  8789  qnegcl  8802  qapne  8805  qdivcl  8809  cnref1o  8814  xnegcl  8975  xltnegi  8978  iccf1o  9102  ige3m2fz  9144  ige2m1fz1  9202  rebtwn2z  9341  flqcl  9355  flapcl  9357  ceilqcl  9390  intfracq  9402  modqcl  9408  mulqmod0  9412  modqdifz  9418  zmodcl  9426  modfzo0difsn  9477  modsumfzodifsn  9478  frec2uzzd  9482  frec2uzsucd  9483  frec2uzuzd  9484  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  frecuzrdgsuctlem  9505  fzofig  9514  iseqovex  9529  iseqvalt  9532  iseqfclt  9536  iseqcaopr3  9556  iser0f  9569  serile  9571  expivallem  9574  exp1  9579  expcl2lemap  9585  m1expcl2  9595  expaddzap  9617  sqcl  9634  nnsqcl  9642  qsqcl  9644  zesq  9688  facp1  9754  faccl  9759  facdiv  9762  bcval  9773  bcrpcl  9777  bcp1n  9785  bcpasc  9790  permnn  9795  sizeennn  9804  sizecl  9805  shftlem  9842  ovshftex  9845  shftf  9856  cjth  9871  imval  9875  recl  9878  imcl  9879  crre  9882  remim  9885  reim0b  9887  cvg1nlemcau  10008  uzin2  10011  resqrexlem1arp  10029  resqrexlemp1rp  10030  resqrexlemglsq  10046  resqrexlemga  10047  resqrtcl  10053  abscl  10075  absrpclap  10085  nn0abscl  10109  fzomaxdiflem  10136  fzomaxdif  10137  maxabslemab  10230  maxcl  10234  minmax  10250  climaddc1  10305  climmulc2  10307  climsubc1  10308  climsubc2  10309  climle  10310  iisermulc2  10316  climlec2  10317  climcvg1nlem  10324  isumrblem  10337  fisumcvg  10338  dvdsval2  10343  sqoddm1div8z  10430  zssinfcl  10488  infssuzex  10489  infssuzcldc  10491  gcdval  10495  gcdn0cl  10498  gcddvds  10499  divgcdnnr  10511  nn0seqcvgd  10567  ialgrlem1st  10568  ialgrlemconst  10569  ialgrp1  10572  eucalgf  10581  eucalglt  10583  lcmval  10589  lcmcllem  10593  lcmgcdlem  10603  cncongr2  10630  sqrt2irrlem  10684  oddpwdclemxy  10691  oddpwdclemdc  10695  qdencn  10943
  Copyright terms: Public domain W3C validator