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

Theorem rspcev 2792
Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
Hypothesis
Ref Expression
rspcv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspcev  |-  ( ( A  e.  B  /\  ps )  ->  E. x  e.  B  ph )
Distinct variable groups:    x, A    x, B    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem rspcev
StepHypRef Expression
1 nfv 1509 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspce 2787 1  |-  ( ( A  e.  B  /\  ps )  ->  E. x  e.  B  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1332    e. wcel 1481   E.wrex 2418
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-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691
This theorem is referenced by:  rspceaimv  2800  rspc2ev  2807  rspc3ev  2809  rspceeqv  2810  reu6i  2878  rspesbca  2996  brralrspcev  3993  nn0suc  4525  elrnmpt1s  4796  elrnrexdm  5566  eldmrexrn  5568  foco2  5662  elabrex  5666  f1elima  5681  fcofo  5692  fliftfun  5704  fliftval  5708  f1oiso2  5735  fo1st  6062  fo2nd  6063  tfr0dm  6226  tfrlemisucaccv  6229  tfrlemi14d  6237  tfrexlem  6238  tfr1onlemsucaccv  6245  tfr1onlemres  6253  tfrcllemsucaccv  6258  tfrcllemres  6266  rdgss  6287  frecabcl  6303  nnaordex  6430  nnawordex  6431  ecelqsg  6489  snfig  6715  nnfi  6773  findcard  6789  fimax2gtrilemstep  6801  unsnfi  6814  eqsupti  6890  supmaxti  6898  supisoex  6903  infminti  6921  finomni  7019  isnumi  7054  oncardval  7058  archnqq  7248  prarloclemarch2  7250  prcdnql  7315  prcunqu  7316  prarloclemlo  7325  prarloclem5  7331  nqprm  7373  1idprl  7421  1idpru  7422  ltexpri  7444  prplnqu  7451  recexprlemm  7455  recexprlem1ssl  7464  recexprlem1ssu  7465  recexpr  7469  aptiprleml  7470  archpr  7474  cauappcvgprlemm  7476  cauappcvgprlemloc  7483  cauappcvgprlem1  7490  cauappcvgprlem2  7491  cauappcvgpr  7493  caucvgprlemm  7499  caucvgprlemloc  7506  caucvgprlem1  7510  caucvgprlem2  7511  caucvgpr  7513  caucvgprprlemmu  7526  caucvgprprlemopl  7528  caucvgprprlemopu  7530  caucvgprprlemloc  7534  caucvgprprlem1  7540  caucvgprprlem2  7541  caucvgprpr  7543  suplocexprlemmu  7549  suplocexprlemloc  7552  suplocexpr  7556  negexsr  7603  recexgt0sr  7604  caucvgsrlemgt1  7626  caucvgsrlemoffres  7631  suplocsrlem  7639  axrnegex  7710  axprecex  7711  nntopi  7725  axcaucvglemres  7730  axpre-suploclemres  7732  cnegex  7963  recexre  8363  recexap  8437  receuap  8453  sup3exmid  8738  cju  8742  nn2ge  8776  nominpos  8980  zdiv  9162  btwnz  9193  supinfneg  9416  infsupneg  9417  ublbneg  9431  lbzbi  9434  zq  9444  z2ge  9638  iccsupr  9778  exbtwnzlemstep  10055  exbtwnzlemex  10057  rebtwn2zlemstep  10060  rebtwn2z  10062  qbtwnre  10064  qbtwnxr  10065  expnbnd  10445  hashunlem  10581  shftlem  10619  shftfvalg  10621  shftfval  10624  caucvgre  10784  cvg1nlemres  10788  rexanuz  10791  rexuz3  10793  resqrexlemex  10828  caubnd2  10920  maxabslemval  11011  maxleast  11016  rexanre  11023  rexico  11024  fimaxre2  11029  minmax  11032  xrmaxiflemval  11050  xrmaxaddlem  11060  xrminmax  11065  climconst  11090  climshftlemg  11102  cn1lem  11114  serf0  11152  zsumdc  11184  fsum3  11187  fsum3cvg3  11196  mertenslemi1  11335  ntrivcvgap0  11349  zproddc  11379  dvdsval2  11530  dvds0lem  11537  dvds1lem  11538  dvds2lem  11539  odd2np1lem  11603  odd2np1  11604  opeo  11628  omeo  11629  divalglemex  11653  zsupcllemstep  11672  infssuzex  11676  bezoutlemnewy  11718  bezoutlemaz  11725  bezoutlembz  11726  bezoutlemsup  11731  ncoprmgcdne1b  11804  exprmfct  11852  ennnfonelemex  11961  ennnfonelemhom  11962  ennnfonelemrn  11966  ennnfonelemnn0  11969  ennnfonelemim  11971  exmidunben  11973  ctinfomlemom  11974  ctinfom  11975  ctinf  11977  ctiunctlemf  11985  fiinbas  12253  topbas  12273  clsval  12317  neiint  12351  neipsm  12360  opnneissb  12361  opnssneib  12362  innei  12369  restbasg  12374  lmconst  12422  iscnp4  12424  cncnpi  12434  cnconst2  12439  cnptoprest  12445  cnpdis  12448  neitx  12474  txcnp  12477  blssps  12633  blss  12634  blssexps  12635  blssex  12636  ssblex  12637  blin2  12638  neibl  12697  metss2  12704  bdmopn  12710  metrest  12712  metcnp3  12717  tgioo  12752  tgqioo  12753  addcncntoplem  12757  cnopnap  12800  dedekindeulemuub  12801  suplociccreex  12808  dedekindicclemuub  12810  ivthinclemlm  12818  ivthinclemum  12819  ivthinclemlopn  12820  ivthinclemuopn  12822  reeff1oleme  12899  sin0pilem2  12909  bj-nn0suc0  13317  bj-inf2vnlem1  13337  nninfsellemeq  13383  nninfomnilem  13387  qdencn  13395  trirec0  13410
  Copyright terms: Public domain W3C validator