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

Theorem eleq1d 2148
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 2142 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 14 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = 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:  eleq12d  2150  eqeltrd  2156  eqneltrd  2175  eqneltrrd  2176  rspcimdv  2703  rspcimedv  2704  reuind  2796  sbcel2g  2928  sbccsb2g  2936  breq1  3796  breq2  3797  inex1g  3922  intexr  3933  pwex  3961  pwexg  3962  prexg  3974  opelopabsb  4023  pofun  4075  seex  4098  uniex  4200  uniexg  4201  unexb  4203  reusv3  4218  rabxfrd  4227  onun2  4242  onsucelsucexmid  4281  ordsucunielexmid  4282  tfisi  4336  peano2  4344  seinxp  4437  opabid2  4495  opeliunxp2  4504  elrn2g  4553  opeldm  4566  opeldmg  4568  elreldm  4588  elrn2  4604  opelresg  4647  elsnres  4675  iss  4684  elimasng  4723  issref  4737  rnxpid  4785  unielrel  4875  dffun5r  4944  funopg  4964  brprcneu  5202  tz6.12f  5234  fvelrnb  5253  ssimaex  5266  dmfco  5273  fvmpt3  5283  mptfvex  5288  fvmptf  5295  respreima  5327  fvelrn  5330  ffnfvf  5356  ffvresb  5360  fmptco  5362  fmptcof  5363  fsn  5367  fressnfv  5382  fnex  5415  funfvima  5422  funfvima3  5424  f1mpt  5442  fliftfuns  5469  isoselem  5490  ffnov  5636  fovcl  5637  ovmpt2s  5655  ov2gf  5656  ovg  5670  funimassov  5681  caovclg  5684  elovmpt2  5732  fnofval  5752  off  5755  fnexALT  5771  fornex  5773  f1stres  5817  f2ndres  5818  xp1st  5823  xp2nd  5824  elxp6  5827  unielxp  5831  fmpt2x  5857  mpt2fvex  5860  dftpos4  5912  smoel  5949  tfrlem3-2d  5961  tfrlem8  5967  tfrlem9  5968  tfrlemibxssdm  5976  tfrlemi1  5981  tfrexlem  5983  tfr1onlemsucfn  5989  tfr1onlemsucaccv  5990  tfr1onlembxssdm  5992  tfr1onlembfn  5993  tfr1onlemaccex  5997  tfr1onlemres  5998  tfri1dALT  6000  tfrcllemsucfn  6002  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllembfn  6006  tfrcllemaccex  6010  tfrcllemres  6011  tfrcl  6013  rdgtfr  6023  rdgon  6035  frecabex  6047  frecabcl  6048  frecfcllem  6053  frecsuclem  6055  nnacl  6124  nnmcl  6125  nnmordi  6155  nnaordex  6166  nnm00  6168  erexb  6197  qliftfuns  6256  fundmen  6353  fopwdom  6380  xpf1o  6385  dif1en  6414  diffitest  6421  diffifi  6428  unfiexmid  6438  unfidisj  6442  fnfi  6446  isnumi  6510  addnidpig  6588  indpi  6594  dfplpq2  6606  addclnq  6627  mulclnq  6628  nnnq0lem1  6698  addclnq0  6703  mulclnq0  6704  nqpnq0nq  6705  distrnq0  6711  prloc  6743  prarloclemlo  6746  prarloclem3  6749  prarloclem5  6752  genpml  6769  genpmu  6770  addnqprl  6781  addnqpru  6782  mulnqprl  6820  mulnqpru  6821  ltexprlemell  6850  ltexprlemelu  6851  ltexprlemdisj  6858  ltexprlemloc  6859  ltexprlemrl  6862  ltexprlemru  6864  ltexpri  6865  recexprlemm  6876  recexprlemdisj  6882  recexprlemloc  6883  recexprlem1ssl  6885  recexprlem1ssu  6886  recexpr  6890  addclsr  6992  mulclsr  6993  pitonn  7078  peano2nnnn  7083  axaddrcl  7095  axmulrcl  7097  peano5nnnn  7120  negreb  7440  negf1o  7553  cju  8105  peano2nn  8118  nn1m1nn  8124  nnaddcl  8126  nnmulcl  8127  nnsub  8144  nndivtr  8147  un0addcl  8388  un0mulcl  8389  elnnnn0  8398  elz  8434  nnnegz  8435  znegclb  8465  zaddcllempos  8469  zaddcllemneg  8471  zaddcl  8472  nzadd  8484  zmulcl  8485  elz2  8500  zneo  8529  nneoor  8530  zeo  8533  peano5uzti  8536  zindd  8546  uzp1  8733  uzaddcl  8755  supinfneg  8764  infsupneg  8765  supminfex  8766  ublbneg  8779  eqreznegel  8780  negm  8781  qmulz  8789  qnegcl  8802  irradd  8812  irrmul  8813  fzrev2  9178  negqmod0  9413  frec2uzuzd  9484  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  frecuzrdgsuctlem  9505  iseqovex  9529  iseqval  9530  iseqvalt  9532  iseq1  9533  iseq1t  9534  iseqfcl  9535  iseqfclt  9536  iseqcl  9537  iseqp1  9538  iseqp1t  9539  iseqoveq  9540  monoord  9551  monoord2  9552  isermono  9553  iseqsplit  9554  iseqcaopr3  9556  iseqcaopr2  9557  iseqid3  9561  iseqhomo  9565  iseqz  9566  iseqdistr  9567  expival  9575  expp1  9580  expcllem  9584  expcl2lemap  9585  m1expcl2  9595  facnn  9751  fac0  9752  fac1  9753  faccl  9759  facdiv  9762  facndiv  9763  bccmpl  9778  bcn2  9788  bccl  9791  focdmex  9811  sizeeqf1oi  9812  shftlem  9842  shftf  9856  cjval  9870  cjth  9871  remim  9885  uzin2  10011  caubnd2  10141  negfi  10248  clim  10258  clim2  10260  climshftlemg  10279  climcn1  10285  climcn2  10286  iiserex  10315  climub  10320  climserile  10321  climcau  10322  serif0  10327  isumrblem  10337  fisumcvg  10338  zeo3  10412  mulsucdiv2z  10429  zob  10435  nn0o1gt2  10449  nno  10450  nn0o  10451  infssuzex  10489  infssuzcldc  10491  znnen  10709  bdinex1g  10850  bj-intexr  10857  bj-prexg  10860  bj-uniex  10866  bj-uniexg  10867  bdunexb  10869  bj-indsuc  10881  qdencn  10943
  Copyright terms: Public domain W3C validator