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

Theorem eleq1d 2186
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eleq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
eleq1d  |-  ( ph  ->  ( A  e.  C  <->  B  e.  C ) )

Proof of Theorem eleq1d
StepHypRef Expression
1 eleq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 eleq1 2180 . 2  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
31, 2syl 14 1  |-  ( ph  ->  ( A  e.  C  <->  B  e.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1316    e. wcel 1465
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113
This theorem is referenced by:  eleq12d  2188  eqeltrd  2194  eqneltrd  2213  eqneltrrd  2214  rspcimdv  2764  rspcimedv  2765  reuind  2862  sbcel2g  2994  sbccsb2g  3002  breq1  3902  breq2  3903  inex1g  4034  intexr  4045  pwexg  4074  prexg  4103  opelopabsb  4152  pofun  4204  seex  4227  uniex  4329  uniexg  4331  unexb  4333  abnexg  4337  reusv3  4351  rabxfrd  4360  onun2  4376  onsucelsucexmid  4415  ordsucunielexmid  4416  dcextest  4465  tfisi  4471  peano2  4479  seinxp  4580  opabid2  4640  opeliunxp2  4649  elrn2g  4699  opeldm  4712  opeldmg  4714  elreldm  4735  elrn2  4751  opelresg  4796  elsnres  4826  iss  4835  elimasng  4877  issref  4891  rnxpid  4943  unielrel  5036  dffun5r  5105  funopg  5127  brprcneu  5382  tz6.12f  5418  fvelrnb  5437  ssimaex  5450  dmfco  5457  fvmpt3  5468  mptfvex  5474  fvmptf  5481  respreima  5516  fvelrn  5519  ffnfvf  5547  ffvresb  5551  fmptco  5554  fmptcof  5555  fsn  5560  fressnfv  5575  fnex  5610  funfvima  5617  funfvima3  5619  f1mpt  5640  fliftfuns  5667  isoselem  5689  ffnov  5843  fovcl  5844  ovmpos  5862  ov2gf  5863  ovg  5877  funimassov  5888  caovclg  5891  elovmpo  5939  off  5962  fnexALT  5979  fornex  5981  f1stres  6025  f2ndres  6026  xp1st  6031  xp2nd  6032  elxp6  6035  oprssdmm  6037  unielxp  6040  fmpox  6066  mpofvex  6069  opeliunxp2f  6103  dftpos4  6128  smoel  6165  tfrlem3-2d  6177  tfrlem8  6183  tfrlem9  6184  tfrlemibxssdm  6192  tfrlemi1  6197  tfrexlem  6199  tfr1onlemsucfn  6205  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlembfn  6209  tfr1onlemaccex  6213  tfr1onlemres  6214  tfri1dALT  6216  tfrcllemsucfn  6218  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllembfn  6222  tfrcllemaccex  6226  tfrcllemres  6227  tfrcl  6229  rdgtfr  6239  rdgon  6251  frecabex  6263  frecabcl  6264  frecfcllem  6269  frecsuclem  6271  nnacl  6344  nnmcl  6345  nnmordi  6380  nnaordex  6391  nnm00  6393  erexb  6422  qliftfuns  6481  ixpsnval  6563  elixp2  6564  resixp  6595  mptelixpg  6596  elixpsn  6597  fundmen  6668  fopwdom  6698  xpf1o  6706  dif1en  6741  diffitest  6749  diffifi  6756  inffiexmid  6768  unfiexmid  6774  unfidisj  6778  fiintim  6785  xpfi  6786  ssfirab  6790  fnfi  6793  iunfidisj  6802  snexxph  6806  fidcenumlemr  6811  elfi2  6828  ctssdccl  6964  isnumi  7006  addnidpig  7112  indpi  7118  dfplpq2  7130  addclnq  7151  mulclnq  7152  nnnq0lem1  7222  addclnq0  7227  mulclnq0  7228  nqpnq0nq  7229  distrnq0  7235  prloc  7267  prarloclemlo  7270  prarloclem3  7273  prarloclem5  7276  genpml  7293  genpmu  7294  addnqprl  7305  addnqpru  7306  mulnqprl  7344  mulnqpru  7345  ltexprlemell  7374  ltexprlemelu  7375  ltexprlemdisj  7382  ltexprlemloc  7383  ltexprlemrl  7386  ltexprlemru  7388  ltexpri  7389  recexprlemm  7400  recexprlemdisj  7406  recexprlemloc  7407  recexprlem1ssl  7409  recexprlem1ssu  7410  recexpr  7414  addclsr  7529  mulclsr  7530  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  suplocsr  7585  pitonn  7624  peano2nnnn  7629  axaddrcl  7641  axmulrcl  7643  peano5nnnn  7668  axpre-suploclemres  7677  negreb  7995  negf1o  8112  eqord1  8213  eqord2  8214  cju  8683  peano2nn  8696  nn1m1nn  8702  nnaddcl  8704  nnmulcl  8705  nnsub  8723  nndivtr  8726  un0addcl  8968  un0mulcl  8969  elnnnn0  8978  elz  9014  nnnegz  9015  znegclb  9045  zaddcllempos  9049  zaddcllemneg  9051  zaddcl  9052  nzadd  9064  zmulcl  9065  elz2  9080  zneo  9110  nneoor  9111  zeo  9114  peano5uzti  9117  zindd  9127  uzp1  9315  uzaddcl  9337  supinfneg  9346  infsupneg  9347  supminfex  9348  ublbneg  9361  eqreznegel  9362  negm  9363  qmulz  9371  qnegcl  9384  irradd  9394  irrmul  9395  fzrev2  9820  negqmod0  10059  frec2uzuzd  10130  frecuzrdgrrn  10136  frec2uzrdg  10137  frecuzrdgrcl  10138  frecuzrdgsuc  10142  frecuzrdgrclt  10143  frecuzrdgg  10144  frecuzrdgsuctlem  10151  iseqovex  10184  seq3val  10186  seqvalcd  10187  seq3-1  10188  seqf  10189  seq3p1  10190  seqovcd  10191  seqp1cd  10194  seq3clss  10195  monoord  10204  monoord2  10205  ser3mono  10206  seq3split  10207  seq3caopr3  10209  seq3caopr2  10210  iseqf1olemjpcl  10223  iseqf1olemqpcl  10224  iseqf1olemfvp  10225  seq3f1olemqsumkj  10226  seq3f1olemqsum  10228  seq3f1oleml  10231  seq3f1o  10232  seq3homo  10238  seq3z  10239  seq3distr  10241  ser3ge0  10245  expp1  10255  expcllem  10259  expcl2lemap  10260  m1expcl2  10270  facnn  10428  fac0  10429  fac1  10430  faccl  10436  facdiv  10439  facndiv  10440  bccmpl  10455  bcn2  10465  bccl  10468  focdmex  10488  fihasheqf1oi  10489  seq3coll  10540  shftlem  10543  shftf  10557  seq3shft  10565  cjval  10572  cjth  10573  remim  10587  uzin2  10714  caubnd2  10844  negfi  10954  xrmaxltsup  10982  clim  11005  clim2  11007  climshftlemg  11026  climcn1  11032  climcn2  11033  iserex  11063  climub  11068  climserle  11069  climcau  11071  serf0  11076  sumfct  11098  sumrbdclem  11100  fsum3cvg  11101  summodclem3  11104  summodclem2a  11105  zsumdc  11108  fsumgcl  11110  fsum3  11111  fsumf1o  11114  isumss  11115  isumss2  11117  fsum3cvg2  11118  fsum3ser  11121  fsumcl2lem  11122  fsumsplitf  11132  sumpr  11137  sumtp  11138  fsumm1  11140  fsum1p  11142  isummulc2  11150  fsum2dlemstep  11158  fisumcom2  11162  fsumshftm  11169  fisum0diag2  11171  fsummulc2  11172  fsumge1  11185  fsum00  11186  fsumabs  11189  telfsumo  11190  telfsumo2  11191  fsumparts  11194  fsumrelem  11195  fsumiun  11201  binomlem  11207  isumshft  11214  isum1p  11216  isumrpcl  11218  cvgratnnlemnexp  11248  cvgratnnlemmn  11249  cvgratnnlemseq  11250  cvgratnnlemabsle  11251  cvgratnnlemfm  11253  cvgratnnlemrate  11254  cvgratnn  11255  cvgratz  11256  mertenslem2  11260  mertensabs  11261  zeo3  11477  mulsucdiv2z  11494  zob  11500  nn0o1gt2  11514  nno  11515  nn0o  11516  infssuzex  11554  infssuzcldc  11556  qnumdencl  11776  znnen  11822  ennnfonelemj0  11825  ennnfonelemg  11827  ennnfonelemom  11832  ctinfom  11852  ctiunctlemu1st  11858  ctiunctlemu2nd  11859  ctiunctlemudc  11861  ctiunctlemfo  11863  isstruct2im  11880  isstruct2r  11881  uniopn  12079  inopn  12081  fiinopn  12082  iscld  12183  iuncld  12195  tgrest  12249  iscn  12277  cnpval  12278  iscnp  12279  tgcn  12288  ssidcn  12290  lmbrf  12295  cnpnei  12299  cnima  12300  cnconst2  12313  cnrest2  12316  cnptopresti  12318  cnptoprest  12319  lmres  12328  lmtopcnp  12330  txbasval  12347  tx1cn  12349  tx2cn  12350  txcnp  12351  txcnmpt  12353  txdis1cn  12358  txlm  12359  cnmpt11  12363  cnmpt12  12367  cnmpt21  12371  cnmpt22  12374  ishmeo  12384  hmeoopn  12391  hmeocld  12392  qtopbasss  12601  fsumcncntop  12636  expcncf  12672  ivthinclemlopn  12694  ivthinclemlr  12695  ivthinclemuopn  12696  ivthinclemur  12697  ivthinclemdisj  12698  ivthinclemloc  12699  ivthinc  12701  ivthdec  12702  limccl  12708  ellimc3apf  12709  cnmptlimc  12723  limccoap  12727  bdinex1g  12995  bj-intexr  13002  bj-prexg  13005  bj-uniex  13011  bj-uniexg  13012  bdunexb  13014  bj-indsuc  13022  exmidsbthrlem  13113  qdencn  13118
  Copyright terms: Public domain W3C validator