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  8687  peano2nn  8700  nn1m1nn  8706  nnaddcl  8708  nnmulcl  8709  nnsub  8727  nndivtr  8730  un0addcl  8978  un0mulcl  8979  elnnnn0  8988  elz  9024  nnnegz  9025  znegclb  9055  zaddcllempos  9059  zaddcllemneg  9061  zaddcl  9062  nzadd  9074  zmulcl  9075  elz2  9090  zneo  9120  nneoor  9121  zeo  9124  peano5uzti  9127  zindd  9137  uzp1  9327  uzaddcl  9349  supinfneg  9358  infsupneg  9359  supminfex  9360  ublbneg  9373  eqreznegel  9374  negm  9375  qmulz  9383  qnegcl  9396  irradd  9406  irrmul  9407  fzrev2  9833  negqmod0  10072  frec2uzuzd  10143  frecuzrdgrrn  10149  frec2uzrdg  10150  frecuzrdgrcl  10151  frecuzrdgsuc  10155  frecuzrdgrclt  10156  frecuzrdgg  10157  frecuzrdgsuctlem  10164  iseqovex  10197  seq3val  10199  seqvalcd  10200  seq3-1  10201  seqf  10202  seq3p1  10203  seqovcd  10204  seqp1cd  10207  seq3clss  10208  monoord  10217  monoord2  10218  ser3mono  10219  seq3split  10220  seq3caopr3  10222  seq3caopr2  10223  iseqf1olemjpcl  10236  iseqf1olemqpcl  10237  iseqf1olemfvp  10238  seq3f1olemqsumkj  10239  seq3f1olemqsum  10241  seq3f1oleml  10244  seq3f1o  10245  seq3homo  10251  seq3z  10252  seq3distr  10254  ser3ge0  10258  expp1  10268  expcllem  10272  expcl2lemap  10273  m1expcl2  10283  facnn  10441  fac0  10442  fac1  10443  faccl  10449  facdiv  10452  facndiv  10453  bccmpl  10468  bcn2  10478  bccl  10481  focdmex  10501  fihasheqf1oi  10502  seq3coll  10553  shftlem  10556  shftf  10570  seq3shft  10578  cjval  10585  cjth  10586  remim  10600  uzin2  10727  caubnd2  10857  negfi  10967  xrmaxltsup  10995  clim  11018  clim2  11020  climshftlemg  11039  climcn1  11045  climcn2  11046  iserex  11076  climub  11081  climserle  11082  climcau  11084  serf0  11089  sumfct  11111  sumrbdclem  11113  fsum3cvg  11114  summodclem3  11117  summodclem2a  11118  zsumdc  11121  fsumgcl  11123  fsum3  11124  fsumf1o  11127  isumss  11128  isumss2  11130  fsum3cvg2  11131  fsum3ser  11134  fsumcl2lem  11135  fsumsplitf  11145  sumpr  11150  sumtp  11151  fsumm1  11153  fsum1p  11155  isummulc2  11163  fsum2dlemstep  11171  fisumcom2  11175  fsumshftm  11182  fisum0diag2  11184  fsummulc2  11185  fsumge1  11198  fsum00  11199  fsumabs  11202  telfsumo  11203  telfsumo2  11204  fsumparts  11207  fsumrelem  11208  fsumiun  11214  binomlem  11220  isumshft  11227  isum1p  11229  isumrpcl  11231  cvgratnnlemnexp  11261  cvgratnnlemmn  11262  cvgratnnlemseq  11263  cvgratnnlemabsle  11264  cvgratnnlemfm  11266  cvgratnnlemrate  11267  cvgratnn  11268  cvgratz  11269  mertenslem2  11273  mertensabs  11274  zeo3  11492  mulsucdiv2z  11509  zob  11515  nn0o1gt2  11529  nno  11530  nn0o  11531  infssuzex  11569  infssuzcldc  11571  qnumdencl  11792  znnen  11838  ennnfonelemj0  11841  ennnfonelemg  11843  ennnfonelemom  11848  ctinfom  11868  ctiunctlemu1st  11874  ctiunctlemu2nd  11875  ctiunctlemudc  11877  ctiunctlemfo  11879  isstruct2im  11896  isstruct2r  11897  uniopn  12095  inopn  12097  fiinopn  12098  iscld  12199  iuncld  12211  tgrest  12265  iscn  12293  cnpval  12294  iscnp  12295  tgcn  12304  ssidcn  12306  lmbrf  12311  cnpnei  12315  cnima  12316  cnconst2  12329  cnrest2  12332  cnptopresti  12334  cnptoprest  12335  lmres  12344  lmtopcnp  12346  txbasval  12363  tx1cn  12365  tx2cn  12366  txcnp  12367  txcnmpt  12369  txdis1cn  12374  txlm  12375  cnmpt11  12379  cnmpt12  12383  cnmpt21  12387  cnmpt22  12390  ishmeo  12400  hmeoopn  12407  hmeocld  12408  qtopbasss  12617  fsumcncntop  12652  expcncf  12688  ivthinclemlopn  12710  ivthinclemlr  12711  ivthinclemuopn  12712  ivthinclemur  12713  ivthinclemdisj  12714  ivthinclemloc  12715  ivthinc  12717  ivthdec  12718  limccl  12724  ellimc3apf  12725  cnmptlimc  12739  limccoap  12743  bdinex1g  13026  bj-intexr  13033  bj-prexg  13036  bj-uniex  13042  bj-uniexg  13043  bdunexb  13045  bj-indsuc  13053  exmidsbthrlem  13144  qdencn  13149
  Copyright terms: Public domain W3C validator