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

Theorem eleq1d 2184
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 2178 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 14 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1314  wcel 1463
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111
This theorem is referenced by:  eleq12d  2186  eqeltrd  2192  eqneltrd  2211  eqneltrrd  2212  rspcimdv  2762  rspcimedv  2763  reuind  2860  sbcel2g  2992  sbccsb2g  3000  breq1  3900  breq2  3901  inex1g  4032  intexr  4043  pwexg  4072  prexg  4101  opelopabsb  4150  pofun  4202  seex  4225  uniex  4327  uniexg  4329  unexb  4331  abnexg  4335  reusv3  4349  rabxfrd  4358  onun2  4374  onsucelsucexmid  4413  ordsucunielexmid  4414  dcextest  4463  tfisi  4469  peano2  4477  seinxp  4578  opabid2  4638  opeliunxp2  4647  elrn2g  4697  opeldm  4710  opeldmg  4712  elreldm  4733  elrn2  4749  opelresg  4794  elsnres  4824  iss  4833  elimasng  4875  issref  4889  rnxpid  4941  unielrel  5034  dffun5r  5103  funopg  5125  brprcneu  5380  tz6.12f  5416  fvelrnb  5435  ssimaex  5448  dmfco  5455  fvmpt3  5466  mptfvex  5472  fvmptf  5479  respreima  5514  fvelrn  5517  ffnfvf  5545  ffvresb  5549  fmptco  5552  fmptcof  5553  fsn  5558  fressnfv  5573  fnex  5608  funfvima  5615  funfvima3  5617  f1mpt  5638  fliftfuns  5665  isoselem  5687  ffnov  5841  fovcl  5842  ovmpos  5860  ov2gf  5861  ovg  5875  funimassov  5886  caovclg  5889  elovmpo  5937  off  5960  fnexALT  5977  fornex  5979  f1stres  6023  f2ndres  6024  xp1st  6029  xp2nd  6030  elxp6  6033  oprssdmm  6035  unielxp  6038  fmpox  6064  mpofvex  6067  opeliunxp2f  6101  dftpos4  6126  smoel  6163  tfrlem3-2d  6175  tfrlem8  6181  tfrlem9  6182  tfrlemibxssdm  6190  tfrlemi1  6195  tfrexlem  6197  tfr1onlemsucfn  6203  tfr1onlemsucaccv  6204  tfr1onlembxssdm  6206  tfr1onlembfn  6207  tfr1onlemaccex  6211  tfr1onlemres  6212  tfri1dALT  6214  tfrcllemsucfn  6216  tfrcllemsucaccv  6217  tfrcllembxssdm  6219  tfrcllembfn  6220  tfrcllemaccex  6224  tfrcllemres  6225  tfrcl  6227  rdgtfr  6237  rdgon  6249  frecabex  6261  frecabcl  6262  frecfcllem  6267  frecsuclem  6269  nnacl  6342  nnmcl  6343  nnmordi  6378  nnaordex  6389  nnm00  6391  erexb  6420  qliftfuns  6479  ixpsnval  6561  elixp2  6562  resixp  6593  mptelixpg  6594  elixpsn  6595  fundmen  6666  fopwdom  6696  xpf1o  6704  dif1en  6739  diffitest  6747  diffifi  6754  inffiexmid  6766  unfiexmid  6772  unfidisj  6776  fiintim  6783  xpfi  6784  ssfirab  6788  fnfi  6791  iunfidisj  6800  snexxph  6804  fidcenumlemr  6809  elfi2  6826  ctssdccl  6962  isnumi  7004  addnidpig  7108  indpi  7114  dfplpq2  7126  addclnq  7147  mulclnq  7148  nnnq0lem1  7218  addclnq0  7223  mulclnq0  7224  nqpnq0nq  7225  distrnq0  7231  prloc  7263  prarloclemlo  7266  prarloclem3  7269  prarloclem5  7272  genpml  7289  genpmu  7290  addnqprl  7301  addnqpru  7302  mulnqprl  7340  mulnqpru  7341  ltexprlemell  7370  ltexprlemelu  7371  ltexprlemdisj  7378  ltexprlemloc  7379  ltexprlemrl  7382  ltexprlemru  7384  ltexpri  7385  recexprlemm  7396  recexprlemdisj  7402  recexprlemloc  7403  recexprlem1ssl  7405  recexprlem1ssu  7406  recexpr  7410  addclsr  7525  mulclsr  7526  suplocsrlemb  7578  suplocsrlempr  7579  suplocsrlem  7580  suplocsr  7581  pitonn  7620  peano2nnnn  7625  axaddrcl  7637  axmulrcl  7639  peano5nnnn  7664  axpre-suploclemres  7673  negreb  7991  negf1o  8108  eqord1  8209  eqord2  8210  cju  8679  peano2nn  8692  nn1m1nn  8698  nnaddcl  8700  nnmulcl  8701  nnsub  8719  nndivtr  8722  un0addcl  8964  un0mulcl  8965  elnnnn0  8974  elz  9010  nnnegz  9011  znegclb  9041  zaddcllempos  9045  zaddcllemneg  9047  zaddcl  9048  nzadd  9060  zmulcl  9061  elz2  9076  zneo  9106  nneoor  9107  zeo  9110  peano5uzti  9113  zindd  9123  uzp1  9311  uzaddcl  9333  supinfneg  9342  infsupneg  9343  supminfex  9344  ublbneg  9357  eqreznegel  9358  negm  9359  qmulz  9367  qnegcl  9380  irradd  9390  irrmul  9391  fzrev2  9816  negqmod0  10055  frec2uzuzd  10126  frecuzrdgrrn  10132  frec2uzrdg  10133  frecuzrdgrcl  10134  frecuzrdgsuc  10138  frecuzrdgrclt  10139  frecuzrdgg  10140  frecuzrdgsuctlem  10147  iseqovex  10180  seq3val  10182  seqvalcd  10183  seq3-1  10184  seqf  10185  seq3p1  10186  seqovcd  10187  seqp1cd  10190  seq3clss  10191  monoord  10200  monoord2  10201  ser3mono  10202  seq3split  10203  seq3caopr3  10205  seq3caopr2  10206  iseqf1olemjpcl  10219  iseqf1olemqpcl  10220  iseqf1olemfvp  10221  seq3f1olemqsumkj  10222  seq3f1olemqsum  10224  seq3f1oleml  10227  seq3f1o  10228  seq3homo  10234  seq3z  10235  seq3distr  10237  ser3ge0  10241  expp1  10251  expcllem  10255  expcl2lemap  10256  m1expcl2  10266  facnn  10424  fac0  10425  fac1  10426  faccl  10432  facdiv  10435  facndiv  10436  bccmpl  10451  bcn2  10461  bccl  10464  focdmex  10484  fihasheqf1oi  10485  seq3coll  10536  shftlem  10539  shftf  10553  seq3shft  10561  cjval  10568  cjth  10569  remim  10583  uzin2  10710  caubnd2  10840  negfi  10950  xrmaxltsup  10978  clim  11001  clim2  11003  climshftlemg  11022  climcn1  11028  climcn2  11029  iserex  11059  climub  11064  climserle  11065  climcau  11067  serf0  11072  sumfct  11094  sumrbdclem  11096  fsum3cvg  11097  summodclem3  11100  summodclem2a  11101  zsumdc  11104  fsumgcl  11106  fsum3  11107  fsumf1o  11110  isumss  11111  isumss2  11113  fsum3cvg2  11114  fsum3ser  11117  fsumcl2lem  11118  fsumsplitf  11128  sumpr  11133  sumtp  11134  fsumm1  11136  fsum1p  11138  isummulc2  11146  fsum2dlemstep  11154  fisumcom2  11158  fsumshftm  11165  fisum0diag2  11167  fsummulc2  11168  fsumge1  11181  fsum00  11182  fsumabs  11185  telfsumo  11186  telfsumo2  11187  fsumparts  11190  fsumrelem  11191  fsumiun  11197  binomlem  11203  isumshft  11210  isum1p  11212  isumrpcl  11214  cvgratnnlemnexp  11244  cvgratnnlemmn  11245  cvgratnnlemseq  11246  cvgratnnlemabsle  11247  cvgratnnlemfm  11249  cvgratnnlemrate  11250  cvgratnn  11251  cvgratz  11252  mertenslem2  11256  mertensabs  11257  zeo3  11472  mulsucdiv2z  11489  zob  11495  nn0o1gt2  11509  nno  11510  nn0o  11511  infssuzex  11549  infssuzcldc  11551  qnumdencl  11771  znnen  11817  ennnfonelemj0  11820  ennnfonelemg  11822  ennnfonelemom  11827  ctinfom  11847  ctiunctlemu1st  11853  ctiunctlemu2nd  11854  ctiunctlemudc  11856  ctiunctlemfo  11858  isstruct2im  11875  isstruct2r  11876  uniopn  12074  inopn  12076  fiinopn  12077  iscld  12178  iuncld  12190  tgrest  12244  iscn  12272  cnpval  12273  iscnp  12274  tgcn  12283  ssidcn  12285  lmbrf  12290  cnpnei  12294  cnima  12295  cnconst2  12308  cnrest2  12311  cnptopresti  12313  cnptoprest  12314  lmres  12323  lmtopcnp  12325  txbasval  12342  tx1cn  12344  tx2cn  12345  txcnp  12346  txcnmpt  12348  txdis1cn  12353  txlm  12354  cnmpt11  12358  cnmpt12  12362  cnmpt21  12366  cnmpt22  12369  ishmeo  12379  hmeoopn  12386  hmeocld  12387  qtopbasss  12596  fsumcncntop  12631  expcncf  12667  ivthinclemlopn  12689  ivthinclemlr  12690  ivthinclemuopn  12691  ivthinclemur  12692  ivthinclemdisj  12693  ivthinclemloc  12694  ivthinc  12696  ivthdec  12697  limccl  12703  ellimc3apf  12704  cnmptlimc  12718  limccoap  12722  bdinex1g  12933  bj-intexr  12940  bj-prexg  12943  bj-uniex  12949  bj-uniexg  12950  bdunexb  12952  bj-indsuc  12960  exmidsbthrlem  13051  qdencn  13056
  Copyright terms: Public domain W3C validator