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

Theorem eleq1d 2103
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eleq1d.1 (φA = B)
Assertion
Ref Expression
eleq1d (φ → (A 𝐶B 𝐶))

Proof of Theorem eleq1d
StepHypRef Expression
1 eleq1d.1 . 2 (φA = B)
2 eleq1 2097 . 2 (A = B → (A 𝐶B 𝐶))
31, 2syl 14 1 (φ → (A 𝐶B 𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1242   wcel 1390
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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033
This theorem is referenced by:  eleq12d  2105  eqeltrd  2111  eqneltrd  2130  eqneltrrd  2131  rspcimdv  2651  rspcimedv  2652  reuind  2738  sbcel2g  2865  sbccsb2g  2873  breq1  3758  breq2  3759  inex1g  3884  intexr  3895  pwex  3923  pwexg  3924  prexgOLD  3937  prexg  3938  opelopabsb  3988  pofun  4040  seex  4057  uniex  4140  uniexg  4141  unexb  4143  reusv3  4158  rabxfrd  4167  onun2  4182  onsucelsucexmid  4215  ordsucunielexmid  4216  tfisi  4253  peano2  4261  seinxp  4354  opabid2  4410  opeliunxp2  4419  elrn2g  4468  opeldm  4481  opeldmg  4483  elreldm  4503  elrn2  4519  opelresg  4562  elsnres  4590  iss  4597  elimasng  4636  issref  4650  rnxpid  4698  unielrel  4788  dffun5r  4857  funopg  4877  brprcneu  5114  tz6.12f  5145  fvelrnb  5164  ssimaex  5177  dmfco  5184  fvmpt3  5194  mptfvex  5199  fvmptf  5206  respreima  5238  fvelrn  5241  ffnfvf  5267  ffvresb  5271  fmptco  5273  fmptcof  5274  fsn  5278  fressnfv  5293  fnex  5326  funfvima  5333  funfvima3  5335  f1mpt  5353  fliftfuns  5381  isoselem  5402  ffnov  5547  fovcl  5548  ovmpt2s  5566  ov2gf  5567  ovg  5581  funimassov  5592  caovclg  5595  elovmpt2  5643  fnofval  5663  off  5666  fnexALT  5682  fornex  5684  f1stres  5728  f2ndres  5729  xp1st  5734  xp2nd  5735  elxp6  5738  unielxp  5742  fmpt2x  5768  mpt2fvex  5771  dftpos4  5819  smoel  5856  tfrlem3-2  5868  tfrlem3-2d  5869  tfrlem8  5875  tfrlem9  5876  tfrlemibxssdm  5882  tfrlemi1  5887  tfrexlem  5889  rdgtfr  5901  rdgon  5913  frecabex  5923  freccl  5932  nnacl  5998  nnmcl  5999  nnmordi  6025  nnaordex  6036  nnm00  6038  erexb  6067  qliftfuns  6126  fundmen  6222  fopwdom  6246  addnidpig  6320  indpi  6326  dfplpq2  6338  addclnq  6359  mulclnq  6360  nnnq0lem1  6429  addclnq0  6434  mulclnq0  6435  nqpnq0nq  6436  distrnq0  6442  prloc  6474  prarloclemlo  6477  prarloclem3  6480  prarloclem5  6483  genpml  6500  genpmu  6501  addnqprl  6512  addnqpru  6513  mulnqprl  6549  mulnqpru  6550  ltexprlemell  6572  ltexprlemelu  6573  ltexprlemdisj  6580  ltexprlemloc  6581  ltexprlemrl  6584  ltexprlemru  6586  ltexpri  6587  recexprlemm  6596  recexprlemdisj  6602  recexprlemloc  6603  recexprlem1ssl  6605  recexprlem1ssu  6606  recexpr  6610  addclsr  6681  mulclsr  6682  pitonn  6744  axaddrcl  6751  axmulrcl  6753  negreb  7072  cju  7694  peano2nn  7707  nn1m1nn  7713  nnaddcl  7715  nnmulcl  7716  nnsub  7733  nndivtr  7736  un0addcl  7991  un0mulcl  7992  elnnnn0  8001  elz  8023  nnnegz  8024  znegclb  8054  zaddcllempos  8058  zaddcllemneg  8060  zaddcl  8061  zmulcl  8073  elz2  8088  zneo  8115  nneoor  8116  zeo  8119  peano5uzti  8122  zindd  8132  uzp1  8282  uzaddcl  8305  ublbneg  8324  eqreznegel  8325  negm  8326  qmulz  8334  qnegcl  8347  irradd  8355  irrmul  8356  fzrev2  8717  frec2uzzd  8867  frec2uzuzd  8869  frecuzrdgrrn  8875  iseqovex  8899  iseqval  8900  iseqfn  8901  iseq1  8902  iseqcl  8903  iseqp1  8904  expival  8911  expp1  8916  expcllem  8920  expcl2lemap  8921  m1expcl2  8931  cjval  9073  cjth  9074  remim  9088  bdinex1g  9356  bj-intexr  9363  bj-prexg  9366  bj-uniex  9372  bj-uniexg  9373  bdunexb  9375  bj-indsuc  9387
  Copyright terms: Public domain W3C validator