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

Theorem eleq1d 2153
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eleq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
eleq1d (𝜑 → (𝐴𝐶𝐵𝐶))

Proof of Theorem eleq1d
StepHypRef Expression
1 eleq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 eleq1 2147 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 14 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = 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:  eleq12d  2155  eqeltrd  2161  eqneltrd  2180  eqneltrrd  2181  rspcimdv  2716  rspcimedv  2717  reuind  2809  sbcel2g  2941  sbccsb2g  2949  breq1  3825  breq2  3826  inex1g  3952  intexr  3963  pwexg  3992  prexg  4014  opelopabsb  4063  pofun  4115  seex  4138  uniex  4240  uniexg  4241  unexb  4243  reusv3  4258  rabxfrd  4267  onun2  4282  onsucelsucexmid  4321  ordsucunielexmid  4322  dcextest  4371  tfisi  4377  peano2  4385  seinxp  4479  opabid2  4537  opeliunxp2  4546  elrn2g  4596  opeldm  4609  opeldmg  4611  elreldm  4631  elrn2  4647  opelresg  4690  elsnres  4718  iss  4727  elimasng  4769  issref  4783  rnxpid  4833  unielrel  4926  dffun5r  4995  funopg  5015  brprcneu  5263  tz6.12f  5298  fvelrnb  5317  ssimaex  5330  dmfco  5337  fvmpt3  5348  mptfvex  5353  fvmptf  5360  respreima  5392  fvelrn  5395  ffnfvf  5422  ffvresb  5426  fmptco  5429  fmptcof  5430  fsn  5434  fressnfv  5449  fnex  5482  funfvima  5489  funfvima3  5491  f1mpt  5513  fliftfuns  5540  isoselem  5562  ffnov  5708  fovcl  5709  ovmpt2s  5727  ov2gf  5728  ovg  5742  funimassov  5753  caovclg  5756  elovmpt2  5804  fnofval  5824  off  5827  fnexALT  5843  fornex  5845  f1stres  5889  f2ndres  5890  xp1st  5895  xp2nd  5896  elxp6  5899  unielxp  5903  fmpt2x  5929  mpt2fvex  5932  dftpos4  5984  smoel  6021  tfrlem3-2d  6033  tfrlem8  6039  tfrlem9  6040  tfrlemibxssdm  6048  tfrlemi1  6053  tfrexlem  6055  tfr1onlemsucfn  6061  tfr1onlemsucaccv  6062  tfr1onlembxssdm  6064  tfr1onlembfn  6065  tfr1onlemaccex  6069  tfr1onlemres  6070  tfri1dALT  6072  tfrcllemsucfn  6074  tfrcllemsucaccv  6075  tfrcllembxssdm  6077  tfrcllembfn  6078  tfrcllemaccex  6082  tfrcllemres  6083  tfrcl  6085  rdgtfr  6095  rdgon  6107  frecabex  6119  frecabcl  6120  frecfcllem  6125  frecsuclem  6127  nnacl  6197  nnmcl  6198  nnmordi  6229  nnaordex  6240  nnm00  6242  erexb  6271  qliftfuns  6330  fundmen  6477  fopwdom  6506  xpf1o  6514  dif1en  6549  diffitest  6557  diffifi  6564  inffiexmid  6576  unfiexmid  6582  unfidisj  6586  xpfi  6593  ssfirab  6596  fnfi  6599  snexxph  6611  isnumi  6757  addnidpig  6842  indpi  6848  dfplpq2  6860  addclnq  6881  mulclnq  6882  nnnq0lem1  6952  addclnq0  6957  mulclnq0  6958  nqpnq0nq  6959  distrnq0  6965  prloc  6997  prarloclemlo  7000  prarloclem3  7003  prarloclem5  7006  genpml  7023  genpmu  7024  addnqprl  7035  addnqpru  7036  mulnqprl  7074  mulnqpru  7075  ltexprlemell  7104  ltexprlemelu  7105  ltexprlemdisj  7112  ltexprlemloc  7113  ltexprlemrl  7116  ltexprlemru  7118  ltexpri  7119  recexprlemm  7130  recexprlemdisj  7136  recexprlemloc  7137  recexprlem1ssl  7139  recexprlem1ssu  7140  recexpr  7144  addclsr  7246  mulclsr  7247  pitonn  7332  peano2nnnn  7337  axaddrcl  7349  axmulrcl  7351  peano5nnnn  7374  negreb  7694  negf1o  7807  cju  8359  peano2nn  8372  nn1m1nn  8378  nnaddcl  8380  nnmulcl  8381  nnsub  8398  nndivtr  8401  un0addcl  8642  un0mulcl  8643  elnnnn0  8652  elz  8688  nnnegz  8689  znegclb  8719  zaddcllempos  8723  zaddcllemneg  8725  zaddcl  8726  nzadd  8738  zmulcl  8739  elz2  8754  zneo  8783  nneoor  8784  zeo  8787  peano5uzti  8790  zindd  8800  uzp1  8987  uzaddcl  9009  supinfneg  9018  infsupneg  9019  supminfex  9020  ublbneg  9033  eqreznegel  9034  negm  9035  qmulz  9043  qnegcl  9056  irradd  9066  irrmul  9067  fzrev2  9432  negqmod0  9669  frec2uzuzd  9740  frecuzrdgrrn  9746  frec2uzrdg  9747  frecuzrdgrcl  9748  frecuzrdgsuc  9752  frecuzrdgrclt  9753  frecuzrdgg  9754  frecuzrdgsuctlem  9761  iseqovex  9790  iseqval  9791  iseqvalt  9793  iseq1  9794  iseq1t  9795  iseqfcl  9796  iseqfclt  9797  iseqcl  9798  iseqp1  9799  iseqp1t  9800  iseqclt  9801  iseqoveq  9802  monoord  9813  monoord2  9814  isermono  9815  iseqsplit  9816  iseqcaopr3  9818  iseqcaopr2  9819  iseqf1olemjpcl  9832  iseqf1olemqpcl  9833  iseqf1olemfvp  9834  iseqf1olemqsumkj  9835  iseqf1olemqsum  9837  iseqf1oleml  9840  iseqf1o  9841  iseqid3  9844  iseqhomo  9848  iseqz  9849  iseqdistr  9850  expival  9859  expp1  9864  expcllem  9868  expcl2lemap  9869  m1expcl2  9879  facnn  10035  fac0  10036  fac1  10037  faccl  10043  facdiv  10046  facndiv  10047  bccmpl  10062  bcn2  10072  bccl  10075  focdmex  10095  fihasheqf1oi  10096  iseqcoll  10147  shftlem  10150  shftf  10164  cjval  10178  cjth  10179  remim  10193  uzin2  10319  caubnd2  10449  negfi  10557  clim  10567  clim2  10569  climshftlemg  10588  climcn1  10594  climcn2  10595  iiserex  10624  climub  10629  climserile  10630  climcau  10631  serif0  10636  sumfct  10658  isumrblem  10660  fisumcvg  10661  isummolem3  10664  isummolem2a  10665  zisum  10668  fisum  10670  fsumf1o  10673  isumss  10674  isumss2  10676  fisumcvg2  10677  fsumcl2lem  10680  fsumsplitf  10690  sumpr  10694  sumtp  10695  fsumm1  10697  fsum1p  10699  zeo3  10774  mulsucdiv2z  10791  zob  10797  nn0o1gt2  10811  nno  10812  nn0o  10813  infssuzex  10851  infssuzcldc  10853  qnumdencl  11071  znnen  11117  bdinex1g  11261  bj-intexr  11268  bj-prexg  11271  bj-uniex  11277  bj-uniexg  11278  bdunexb  11280  bj-indsuc  11292  exmidsbthrlem  11381  qdencn  11384
  Copyright terms: Public domain W3C validator