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

Theorem eleq1d 2206
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 2200 . 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 1331    e. wcel 1480
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119
This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133
This theorem is referenced by:  eleq12d  2208  eqeltrd  2214  eqneltrd  2233  eqneltrrd  2234  rspcimdv  2785  rspcimedv  2786  reuind  2884  sbcel2g  3018  sbccsb2g  3027  breq1  3927  breq2  3928  inex1g  4059  intexr  4070  pwexg  4099  prexg  4128  opelopabsb  4177  pofun  4229  seex  4252  uniex  4354  uniexg  4356  unexb  4358  abnexg  4362  reusv3  4376  rabxfrd  4385  onun2  4401  onsucelsucexmid  4440  ordsucunielexmid  4441  dcextest  4490  tfisi  4496  peano2  4504  seinxp  4605  opabid2  4665  opeliunxp2  4674  elrn2g  4724  opeldm  4737  opeldmg  4739  elreldm  4760  elrn2  4776  opelresg  4821  elsnres  4851  iss  4860  elimasng  4902  issref  4916  rnxpid  4968  unielrel  5061  dffun5r  5130  funopg  5152  brprcneu  5407  tz6.12f  5443  fvelrnb  5462  ssimaex  5475  dmfco  5482  fvmpt3  5493  mptfvex  5499  fvmptf  5506  respreima  5541  fvelrn  5544  ffnfvf  5572  ffvresb  5576  fmptco  5579  fmptcof  5580  fsn  5585  fressnfv  5600  fnex  5635  funfvima  5642  funfvima3  5644  f1mpt  5665  fliftfuns  5692  isoselem  5714  ffnov  5868  fovcl  5869  ovmpos  5887  ov2gf  5888  ovg  5902  funimassov  5913  caovclg  5916  elovmpo  5964  off  5987  fnexALT  6004  fornex  6006  f1stres  6050  f2ndres  6051  xp1st  6056  xp2nd  6057  elxp6  6060  oprssdmm  6062  unielxp  6065  fmpox  6091  mpofvex  6094  opeliunxp2f  6128  dftpos4  6153  smoel  6190  tfrlem3-2d  6202  tfrlem8  6208  tfrlem9  6209  tfrlemibxssdm  6217  tfrlemi1  6222  tfrexlem  6224  tfr1onlemsucfn  6230  tfr1onlemsucaccv  6231  tfr1onlembxssdm  6233  tfr1onlembfn  6234  tfr1onlemaccex  6238  tfr1onlemres  6239  tfri1dALT  6241  tfrcllemsucfn  6243  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllembfn  6247  tfrcllemaccex  6251  tfrcllemres  6252  tfrcl  6254  rdgtfr  6264  rdgon  6276  frecabex  6288  frecabcl  6289  frecfcllem  6294  frecsuclem  6296  nnacl  6369  nnmcl  6370  nnmordi  6405  nnaordex  6416  nnm00  6418  erexb  6447  qliftfuns  6506  ixpsnval  6588  elixp2  6589  resixp  6620  mptelixpg  6621  elixpsn  6622  fundmen  6693  fopwdom  6723  xpf1o  6731  dif1en  6766  diffitest  6774  diffifi  6781  inffiexmid  6793  unfiexmid  6799  unfidisj  6803  fiintim  6810  xpfi  6811  ssfirab  6815  fnfi  6818  iunfidisj  6827  snexxph  6831  fidcenumlemr  6836  elfi2  6853  ctssdccl  6989  isnumi  7031  addnidpig  7137  indpi  7143  dfplpq2  7155  addclnq  7176  mulclnq  7177  nnnq0lem1  7247  addclnq0  7252  mulclnq0  7253  nqpnq0nq  7254  distrnq0  7260  prloc  7292  prarloclemlo  7295  prarloclem3  7298  prarloclem5  7301  genpml  7318  genpmu  7319  addnqprl  7330  addnqpru  7331  mulnqprl  7369  mulnqpru  7370  ltexprlemell  7399  ltexprlemelu  7400  ltexprlemdisj  7407  ltexprlemloc  7408  ltexprlemrl  7411  ltexprlemru  7413  ltexpri  7414  recexprlemm  7425  recexprlemdisj  7431  recexprlemloc  7432  recexprlem1ssl  7434  recexprlem1ssu  7435  recexpr  7439  addclsr  7554  mulclsr  7555  suplocsrlemb  7607  suplocsrlempr  7608  suplocsrlem  7609  suplocsr  7610  pitonn  7649  peano2nnnn  7654  axaddrcl  7666  axmulrcl  7668  peano5nnnn  7693  axpre-suploclemres  7702  negreb  8020  negf1o  8137  eqord1  8238  eqord2  8239  cju  8712  peano2nn  8725  nn1m1nn  8731  nnaddcl  8733  nnmulcl  8734  nnsub  8752  nndivtr  8755  un0addcl  9003  un0mulcl  9004  elnnnn0  9013  elz  9049  nnnegz  9050  znegclb  9080  zaddcllempos  9084  zaddcllemneg  9086  zaddcl  9087  nzadd  9099  zmulcl  9100  elz2  9115  zneo  9145  nneoor  9146  zeo  9149  peano5uzti  9152  zindd  9162  uzp1  9352  uzaddcl  9374  supinfneg  9383  infsupneg  9384  supminfex  9385  ublbneg  9398  eqreznegel  9399  negm  9400  qmulz  9408  qnegcl  9421  irradd  9431  irrmul  9432  fzrev2  9858  negqmod0  10097  frec2uzuzd  10168  frecuzrdgrrn  10174  frec2uzrdg  10175  frecuzrdgrcl  10176  frecuzrdgsuc  10180  frecuzrdgrclt  10181  frecuzrdgg  10182  frecuzrdgsuctlem  10189  iseqovex  10222  seq3val  10224  seqvalcd  10225  seq3-1  10226  seqf  10227  seq3p1  10228  seqovcd  10229  seqp1cd  10232  seq3clss  10233  monoord  10242  monoord2  10243  ser3mono  10244  seq3split  10245  seq3caopr3  10247  seq3caopr2  10248  iseqf1olemjpcl  10261  iseqf1olemqpcl  10262  iseqf1olemfvp  10263  seq3f1olemqsumkj  10264  seq3f1olemqsum  10266  seq3f1oleml  10269  seq3f1o  10270  seq3homo  10276  seq3z  10277  seq3distr  10279  ser3ge0  10283  expp1  10293  expcllem  10297  expcl2lemap  10298  m1expcl2  10308  facnn  10466  fac0  10467  fac1  10468  faccl  10474  facdiv  10477  facndiv  10478  bccmpl  10493  bcn2  10503  bccl  10506  focdmex  10526  fihasheqf1oi  10527  seq3coll  10578  shftlem  10581  shftf  10595  seq3shft  10603  cjval  10610  cjth  10611  remim  10625  uzin2  10752  caubnd2  10882  negfi  10992  xrmaxltsup  11020  clim  11043  clim2  11045  climshftlemg  11064  climcn1  11070  climcn2  11071  iserex  11101  climub  11106  climserle  11107  climcau  11109  serf0  11114  sumfct  11136  sumrbdclem  11138  fsum3cvg  11139  summodclem3  11142  summodclem2a  11143  zsumdc  11146  fsumgcl  11148  fsum3  11149  fsumf1o  11152  isumss  11153  isumss2  11155  fsum3cvg2  11156  fsum3ser  11159  fsumcl2lem  11160  fsumsplitf  11170  sumpr  11175  sumtp  11176  fsumm1  11178  fsum1p  11180  isummulc2  11188  fsum2dlemstep  11196  fisumcom2  11200  fsumshftm  11207  fisum0diag2  11209  fsummulc2  11210  fsumge1  11223  fsum00  11224  fsumabs  11227  telfsumo  11228  telfsumo2  11229  fsumparts  11232  fsumrelem  11233  fsumiun  11239  binomlem  11245  isumshft  11252  isum1p  11254  isumrpcl  11256  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  cvgratnnlemseq  11288  cvgratnnlemabsle  11289  cvgratnnlemfm  11291  cvgratnnlemrate  11292  cvgratnn  11293  cvgratz  11294  mertenslem2  11298  mertensabs  11299  clim2prod  11301  prodfap0  11307  prodfrecap  11308  prodfdivap  11309  prodrbdclem  11333  fproddccvg  11334  zeo3  11554  mulsucdiv2z  11571  zob  11577  nn0o1gt2  11591  nno  11592  nn0o  11593  infssuzex  11631  infssuzcldc  11633  qnumdencl  11854  znnen  11900  ennnfonelemj0  11903  ennnfonelemg  11905  ennnfonelemom  11910  ctinfom  11930  ctiunctlemu1st  11936  ctiunctlemu2nd  11937  ctiunctlemudc  11939  ctiunctlemfo  11941  isstruct2im  11958  isstruct2r  11959  uniopn  12157  inopn  12159  fiinopn  12160  iscld  12261  iuncld  12273  tgrest  12327  iscn  12355  cnpval  12356  iscnp  12357  tgcn  12366  ssidcn  12368  lmbrf  12373  cnpnei  12377  cnima  12378  cnconst2  12391  cnrest2  12394  cnptopresti  12396  cnptoprest  12397  lmres  12406  lmtopcnp  12408  txbasval  12425  tx1cn  12427  tx2cn  12428  txcnp  12429  txcnmpt  12431  txdis1cn  12436  txlm  12437  cnmpt11  12441  cnmpt12  12445  cnmpt21  12449  cnmpt22  12452  ishmeo  12462  hmeoopn  12469  hmeocld  12470  qtopbasss  12679  fsumcncntop  12714  expcncf  12750  ivthinclemlopn  12772  ivthinclemlr  12773  ivthinclemuopn  12774  ivthinclemur  12775  ivthinclemdisj  12776  ivthinclemloc  12777  ivthinc  12779  ivthdec  12780  limccl  12786  ellimc3apf  12787  cnmptlimc  12801  limccoap  12805  bdinex1g  13088  bj-intexr  13095  bj-prexg  13098  bj-uniex  13104  bj-uniexg  13105  bdunexb  13107  bj-indsuc  13115  exmidsbthrlem  13206  qdencn  13211
  Copyright terms: Public domain W3C validator