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

Theorem rspc 2755
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
Hypotheses
Ref Expression
rspc.1  |-  F/ x ps
rspc.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspc  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hints:    ph( x)    ps( x)

Proof of Theorem rspc
StepHypRef Expression
1 df-ral 2396 . 2  |-  ( A. x  e.  B  ph  <->  A. x
( x  e.  B  ->  ph ) )
2 nfcv 2256 . . . 4  |-  F/_ x A
3 nfv 1491 . . . . 5  |-  F/ x  A  e.  B
4 rspc.1 . . . . 5  |-  F/ x ps
53, 4nfim 1534 . . . 4  |-  F/ x
( A  e.  B  ->  ps )
6 eleq1 2178 . . . . 5  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
7 rspc.2 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
86, 7imbi12d 233 . . . 4  |-  ( x  =  A  ->  (
( x  e.  B  ->  ph )  <->  ( A  e.  B  ->  ps )
) )
92, 5, 8spcgf 2740 . . 3  |-  ( A  e.  B  ->  ( A. x ( x  e.  B  ->  ph )  -> 
( A  e.  B  ->  ps ) ) )
109pm2.43a 51 . 2  |-  ( A  e.  B  ->  ( A. x ( x  e.  B  ->  ph )  ->  ps ) )
111, 10syl5bi 151 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   A.wal 1312    = wceq 1314   F/wnf 1419    e. wcel 1463   A.wral 2391
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-v 2660
This theorem is referenced by:  rspcv  2757  rspc2  2772  pofun  4202  omsinds  4503  fmptcof  5553  fliftfuns  5665  qliftfuns  6479  xpf1o  6704  finexdc  6762  ssfirab  6788  iunfidisj  6800  lble  8665  exfzdc  9968  uzsinds  10166  sumeq2  11079  sumfct  11094  sumrbdclem  11096  summodclem3  11100  summodclem2a  11101  zsumdc  11104  fsumgcl  11106  fsum3  11107  fsumf1o  11110  isumss  11111  isumss2  11113  fsum3cvg2  11114  fsumadd  11126  isummulc2  11146  fsum2dlemstep  11154  fisumcom2  11158  fsumshftm  11165  fisum0diag2  11167  fsummulc2  11168  fsum00  11182  fsumabs  11185  fsumrelem  11191  fsumiun  11197  isumshft  11210  mertenslem2  11256  zsupcllemstep  11545  infssuzex  11549  bezoutlemmain  11593  ctiunctlemudc  11856  iuncld  12190  txcnp  12346  fsumcncntop  12631  bj-nntrans  12983
  Copyright terms: Public domain W3C validator