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

Theorem eqeltrd 2194
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 2186 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 166 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316  wcel 1465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113
This theorem is referenced by:  eqeltrrd  2195  3eltr4d  2201  eqeltrid  2204  syl6eqel  2208  ifcldadc  3471  ifcldcd  3477  intab  3770  disjiun  3894  iinexgm  4049  opexg  4120  tfisi  4471  nnpredcl  4506  imain  5175  fvmptd  5470  fvmptdf  5476  fvmptt  5480  elfvmptrab  5484  dffo3  5535  resfunexg  5609  f1oiso2  5696  riota2df  5718  riota5f  5722  ovmpodxf  5864  ovmpodf  5870  offval  5957  ofvalg  5959  offeq  5963  iunexg  5985  oprabexd  5993  fo1stresm  6027  fo2ndresm  6028  oprssdmm  6037  1stdm  6048  1stconst  6086  2ndconst  6087  cnvf1olem  6089  fo2ndf  6092  f1od2  6100  iunon  6149  tfrlemibacc  6191  tfrlemibfn  6193  tfr1onlembacc  6207  tfr1onlembfn  6209  tfrcllembacc  6220  tfrcllembfn  6222  tfrcl  6229  rdgon  6251  frec0g  6262  freccllem  6267  frecfcllem  6269  frecsuclem  6271  oacl  6324  omcl  6325  oeicl  6326  nntr2  6367  mptelixpg  6596  fidifsnen  6732  en2eqpr  6769  unfiin  6782  ssfirab  6790  fnfi  6793  relcnvfi  6797  fidcenumlemr  6811  elfi2  6828  supclti  6853  supubti  6854  suplubti  6855  supelti  6857  ordiso2  6888  djulclr  6902  djurclr  6903  djulcl  6904  djurcl  6905  djuss  6923  updjudhcoinlf  6933  updjudhcoinrg  6934  ctssdclemn0  6963  ctssdccl  6964  ctssdc  6966  enumctlemm  6967  cardcl  7005  addclpi  7103  mulclpi  7104  addclnq  7151  mulclnq  7152  addclnq0  7227  mulclnq0  7228  nqpnq0nq  7229  elnp1st2nd  7252  prarloclemcalc  7278  distrlem1prl  7358  distrlem1pru  7359  ltexprlemopl  7377  ltexprlemopu  7379  ltexprlemfl  7385  ltexprlemrl  7386  ltexprlemfu  7387  ltexprlemru  7388  addcanprlemu  7391  recexprlemloc  7407  aptiprleml  7415  caucvgprprlemopl  7473  suplocexprlemex  7498  addclsr  7529  mulclsr  7530  recexgt0sr  7549  mulextsr1lem  7556  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  axaddcl  7640  axaddrcl  7641  axmulcl  7642  axmulrcl  7643  axcaucvglemval  7673  subcl  7929  cru  8332  aprcl  8376  divclap  8406  redivclap  8459  diveqap1bd  8563  lbinfcl  8675  cju  8687  nn1m1nn  8706  nnsub  8727  nnnn0addcl  8975  un0addcl  8978  peano2z  9058  peano2zm  9060  zaddcllemneg  9061  zaddcl  9062  nnaddm1cl  9083  nn0n0n1ge2  9089  zdivadd  9108  zdivmul  9109  suprzclex  9117  zneo  9120  peano5uzti  9127  supinfneg  9358  infsupneg  9359  qmulz  9383  qnegcl  9396  qapne  9399  qdivcl  9403  cnref1o  9408  xnegcl  9583  xltnegi  9586  xaddnemnf  9608  xaddnepnf  9609  xnegdi  9619  xnpcan  9623  xltadd1  9627  xposdif  9633  xleaddadd  9638  iccf1o  9755  ige3m2fz  9797  ige2m1fz1  9857  rebtwn2z  10000  flqcl  10014  flapcl  10016  ceilqcl  10049  intfracq  10061  modqcl  10067  mulqmod0  10071  modqdifz  10077  zmodcl  10085  modfzo0difsn  10136  modsumfzodifsn  10137  frec2uzzd  10141  frec2uzsucd  10142  frec2uzuzd  10143  frecuzrdgrrn  10149  frec2uzrdg  10150  frecuzrdgrcl  10151  frecuzrdgsuc  10155  frecuzrdgrclt  10156  frecuzrdgg  10157  frecuzrdgsuctlem  10164  fzofig  10173  iseqovex  10197  seq3val  10199  seqvalcd  10200  seqf  10202  seqovcd  10204  seq3clss  10208  seq3caopr3  10222  iseqf1olemnab  10229  iseqf1olemqk  10235  iseqf1olemjpcl  10236  iseqf1olemqpcl  10237  iseqf1olemfvp  10238  seq3f1olemqsumkj  10239  seq3f1olemqsum  10241  seq3f1oleml  10244  seq3f1o  10245  seq3distr  10254  ser0f  10256  ser3le  10259  exp3vallem  10262  exp3val  10263  exp1  10267  expcl2lemap  10273  m1expcl2  10283  expaddzap  10305  sqcl  10322  nnsqcl  10330  qsqcl  10332  zesq  10378  facp1  10444  faccl  10449  facdiv  10452  bcval  10463  bcrpcl  10467  bcp1n  10475  bcpasc  10480  permnn  10485  hashennn  10494  hashcl  10495  shftlem  10556  ovshftex  10559  shftf  10570  seq3shft  10578  cjth  10586  imval  10590  recl  10593  imcl  10594  crre  10597  remim  10600  reim0b  10602  cvg1nlemcau  10724  uzin2  10727  resqrexlem1arp  10745  resqrexlemp1rp  10746  resqrexlemglsq  10762  resqrexlemga  10763  resqrtcl  10769  abscl  10791  absrpclap  10801  nn0abscl  10825  fzomaxdiflem  10852  fzomaxdif  10853  maxabslemab  10946  maxcl  10950  zmaxcl  10964  minmax  10969  mincl  10970  xrmaxcl  10989  xrmaxaddlem  10997  xrminmax  11002  xrmincl  11003  xrmineqinf  11006  xrminrpcl  11011  reccn2ap  11050  climaddc1  11066  climmulc2  11068  climsubc1  11069  climsubc2  11070  climle  11071  climlec2  11078  climcvg1nlem  11086  sumrbdclem  11113  fsum3cvg  11114  summodclem3  11117  summodclem2a  11118  zsumdc  11121  fsumgcl  11123  fsum3  11124  isumss  11128  fisumss  11129  isumss2  11130  fsum3cvg2  11131  fsum3ser  11134  fsumcl2lem  11135  fsumcllem  11136  fsumadd  11143  sumsnf  11146  fsumsplitsn  11147  isumcl  11162  isummulc2  11163  isumrecl  11166  isumge0  11167  isumadd  11168  fsum2dlemstep  11171  fisumcom2  11175  mptfzshft  11179  fsumrev  11180  fsummulc2  11185  iserabs  11212  isumshft  11227  isumsplit  11228  isum1p  11229  isumrpcl  11231  isumle  11232  isumlessdc  11233  trireciplem  11237  expcnvap0  11239  expcnvre  11240  expcnv  11241  explecnv  11242  geolim  11248  geolim2  11249  geo2lim  11253  cvgratnnlemsumlt  11265  cvgratz  11269  mertenslemub  11271  mertenslemi1  11272  mertenslem2  11273  mertensabs  11274  efcllemp  11291  ef0lem  11293  efcvgfsum  11300  reefcl  11301  ege2le3  11304  efcj  11306  efaddlem  11307  eftlcvg  11320  eftlcl  11321  reeftlcl  11322  eftlub  11323  efsep  11324  effsumlt  11325  efgt1p2  11328  efgt1p  11329  reeff1  11334  tanclap  11343  resincl  11354  recoscl  11355  retanclap  11356  eirraplem  11410  dvdsval2  11423  sqoddm1div8z  11510  zssinfcl  11568  infssuzex  11569  infssuzcldc  11571  gcdval  11575  gcdn0cl  11578  gcddvds  11579  divgcdnnr  11591  nn0seqcvgd  11649  ialgrlem1st  11650  ialgrlemconst  11651  algrf  11653  algrp1  11654  eucalgf  11663  eucalglt  11665  lcmval  11671  lcmcllem  11675  lcmgcdlem  11685  cncongr2  11712  sqrt2irrlem  11766  oddpwdclemxy  11774  oddpwdclemdc  11778  qden1elz  11810  phicl2  11817  phimullem  11828  ennnfonelemjn  11842  ennnfonelemg  11843  ennnfonelemp1  11846  ctinfomlemom  11867  ctiunctlemfo  11879  setsex  11918  strsetsid  11919  ressid2  11945  ressval2  11946  ressid  11947  iunopn  12096  toponmax  12119  tgvalex  12146  tgtop  12164  tgiun  12169  tgidm  12170  ntropn  12213  tgrest  12265  restopnb  12277  cnovex  12292  cnclima  12319  txvalex  12350  txtop  12356  tx1cn  12365  tx2cn  12366  txcnp  12367  txcnmpt  12369  txdis1cn  12374  cnmptcom  12394  imasnopn  12395  hmeocnv  12403  hmeores  12411  txhmeo  12415  txswaphmeo  12417  ispsmet  12419  xmetres  12478  metres  12479  blex  12483  xmeter  12532  xmetresbl  12536  mopntopon  12539  isxms2  12548  xmetxp  12603  xmettx  12606  txmetcnp  12614  qtopbasss  12617  qtopbas  12618  reopnap  12634  ioo2blex  12640  blssioo  12641  tgioo  12642  fsumcncntop  12652  cncfval  12655  divccncfap  12673  cdivcncfap  12683  ivthdec  12718  limccnpcntop  12740  dvrecap  12773  pilem3  12791  tanrpcl  12845  cosordlem  12857  djucllem  12934  nninfsellemeq  13137  qdencn  13149  isomninnlem  13152  cvgcmp2nlemabs  13154  trilpolemclim  13156  trilpolemisumle  13158  trilpolemeq1  13160  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator