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

Theorem eleq1d 2080
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 2074 . 2 (A = B → (A 𝐶B 𝐶))
31, 2syl 14 1 (φ → (A 𝐶B 𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1224   wcel 1367
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 1310  ax-gen 1312  ax-ie1 1356  ax-ie2 1357  ax-4 1374  ax-17 1393  ax-ial 1401  ax-ext 1996
This theorem depends on definitions:  df-bi 110  df-cleq 2007  df-clel 2010
This theorem is referenced by:  eleq12d  2082  eqeltrd  2088  eqneltrd  2107  eqneltrrd  2108  rspcimdv  2626  rspcimedv  2627  reuind  2713  sbcel2g  2840  sbccsb2g  2848  breq1  3731  breq2  3732  inex1g  3857  intexr  3868  pwex  3896  pwexg  3897  prexgOLD  3910  prexg  3911  opelopabsb  3961  pofun  4013  seex  4030  uniex  4113  uniexg  4114  unexb  4116  reusv3  4131  rabxfrd  4140  onun2  4155  onsucelsucexmid  4188  ordsucunielexmid  4189  tfisi  4226  peano2  4234  seinxp  4327  opabid2  4383  opeliunxp2  4392  elrn2g  4441  opeldm  4454  opeldmg  4456  elreldm  4476  elrn2  4492  opelresg  4535  elsnres  4563  iss  4570  elimasng  4609  issref  4623  rnxpid  4671  unielrel  4761  funopg  4849  brprcneu  5085  tz6.12f  5116  fvelrnb  5135  ssimaex  5148  dmfco  5155  fvmpt3  5165  mptfvex  5170  fvmptf  5177  respreima  5209  fvelrn  5212  ffnfvf  5238  ffvresb  5242  fmptco  5244  fmptcof  5245  fsn  5249  fressnfv  5264  fnex  5297  funfvima  5304  funfvima3  5306  f1mpt  5324  fliftfuns  5352  isoselem  5373  ffnov  5517  fovcl  5518  ovmpt2s  5536  ov2gf  5537  ovg  5551  funimassov  5562  caovclg  5565  elovmpt2  5613  fnofval  5633  off  5636  fnexALT  5652  fornex  5654  f1stres  5698  f2ndres  5699  xp1st  5704  xp2nd  5705  elxp6  5708  unielxp  5712  fmpt2x  5738  mpt2fvex  5741  dftpos4  5789  smoel  5826  tfrlem3-2  5838  tfrlem3-2d  5839  tfrlem8  5845  tfrlem9  5846  tfrlemibxssdm  5851  tfrlemi1  5856  tfrexlem  5859  rdgon  5882  nnacl  5963  nnmcl  5964  nnmordi  5989  nnaordex  6000  nnm00  6002  erexb  6031  qliftfuns  6090  addnidpig  6183  dfplpq2  6200  addclnq  6221  mulclnq  6222  nnnq0lem1  6288  addclnq0  6293  mulclnq0  6294  nqpnq0nq  6295  distrnq0  6301  prloc  6332  prarloclemlo  6335  prarloclem3  6338  prarloclem5  6341  genpml  6359  genpmu  6360  addnqprl  6371  addnqpru  6372  mulnqprl  6399  mulnqpru  6400  ltexprlemell  6422  ltexprlemelu  6423  ltexprlemdisj  6430  ltexprlemloc  6431  ltexprlemrl  6434  ltexprlemru  6436  ltexpri  6437  recexprlemm  6446  recexprlemdisj  6452  recexprlemloc  6453  recexprlem1ssl  6455  recexprlem1ssu  6456  recexpr  6460  addclsr  6492  mulclsr  6493  axaddrcl  6557  axmulrcl  6559  negreb  6876  cju  7497  peano2nn  7510  nn1m1nn  7516  nnaddcl  7518  nnmulcl  7519  nnsub  7536  nndivtr  7539  un0addcl  7790  un0mulcl  7791  elnnnn0  7800  elz  7822  nnnegz  7823  znegclb  7852  zaddcllempos  7856  zaddcllemneg  7858  zaddcl  7859  zmulcl  7869  zneo  7905  nneoor  7906  zeo  7909  peano5uzti  7912  zindd  7922  qmulz  8042  qnegcl  8055  irradd  8063  irrmul  8064  bdinex1g  8354  bj-intexr  8361  bj-prexg  8364  bj-uniex  8370  bj-uniexg  8371  bdunexb  8373  bj-indsuc  8385
  Copyright terms: Public domain W3C validator