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

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

Proof of Theorem rspcv
StepHypRef Expression
1 nfv 1437 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 2667 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102    = wceq 1259    e. wcel 1409   A.wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-v 2576
This theorem is referenced by:  rspccv  2670  rspcva  2671  rspccva  2672  rspcda  2678  rspc3v  2688  rr19.3v  2705  rr19.28v  2706  rspsbc  2868  intmin  3663  frirrg  4115  ralxfrALT  4227  ontr2exmid  4278  reg2exmidlema  4287  0elsucexmid  4317  wetriext  4329  funcnvuni  4996  acexmidlemcase  5535  grprinvlem  5723  grprinvd  5724  caofref  5760  tfrlem1  5954  tfrlem5  5961  tfrlem9  5966  rdgon  6004  nneneq  6351  diffitest  6375  ordiso2  6415  prltlu  6643  prnmaxl  6644  prnminu  6645  cauappcvgprlemm  6801  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  caucvgprlemm  6824  caucvgprprlemml  6850  caucvgsrlemcl  6931  caucvgsrlemfv  6933  caucvgsr  6944  axcaucvglemres  7031  nnsub  8028  ublbneg  8645  fzrevral  9069  iseqovex  9383  iseqval  9384  iseqfn  9385  iseq1  9386  iseqcl  9387  iseqp1  9389  iseqfveq2  9392  iseqfveq  9394  iseqfeq  9395  iseqshft2  9396  monoord  9399  monoord2  9400  isermono  9401  iseqsplit  9402  iseqcaopr3  9404  iseqid3s  9410  iseqid  9411  iseqhomo  9412  cvg1nlemcau  9811  cvg1nlemres  9812  recvguniq  9822  resqrexlemgt0  9847  resqrexlemoverl  9848  resqrexlemglsq  9849  recan  9936  cau3lem  9941  caubnd2  9944  climi  10039  climshftlemg  10054  climcn1  10060  subcn2  10063  climcau  10097  serif0  10102  ndvdssub  10242  sqrt2irr  10251  bj-indsuc  10439  bj-inf2vnlem2  10483
  Copyright terms: Public domain W3C validator