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

Theorem rspc 2716
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 2364 . 2  |-  ( A. x  e.  B  ph  <->  A. x
( x  e.  B  ->  ph ) )
2 nfcv 2228 . . . 4  |-  F/_ x A
3 nfv 1466 . . . . 5  |-  F/ x  A  e.  B
4 rspc.1 . . . . 5  |-  F/ x ps
53, 4nfim 1509 . . . 4  |-  F/ x
( A  e.  B  ->  ps )
6 eleq1 2150 . . . . 5  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
7 rspc.2 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
86, 7imbi12d 232 . . . 4  |-  ( x  =  A  ->  (
( x  e.  B  ->  ph )  <->  ( A  e.  B  ->  ps )
) )
92, 5, 8spcgf 2701 . . 3  |-  ( A  e.  B  ->  ( A. x ( x  e.  B  ->  ph )  -> 
( A  e.  B  ->  ps ) ) )
109pm2.43a 50 . 2  |-  ( A  e.  B  ->  ( A. x ( x  e.  B  ->  ph )  ->  ps ) )
111, 10syl5bi 150 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   A.wal 1287    = wceq 1289   F/wnf 1394    e. wcel 1438   A.wral 2359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-v 2621
This theorem is referenced by:  rspcv  2718  rspc2  2731  pofun  4130  omsinds  4425  fmptcof  5449  fliftfuns  5559  qliftfuns  6356  xpf1o  6540  finexdc  6598  ssfirab  6622  iunfidisj  6634  lble  8380  exfzdc  9616  uzsinds  9813  sumeq2  10712  sumfct  10727  isumrblem  10729  isummolem3  10734  isummolem2a  10735  zisum  10738  fsumgcl  10741  fisum  10742  fsumf1o  10746  isumss  10747  isumss2  10749  fisumcvg2  10750  fsumadd  10763  isummulc2  10783  fsum2dlemstep  10791  fisumcom2  10795  fsumshftm  10802  fisum0diag2  10804  fsummulc2  10805  fsum00  10819  fsumabs  10822  fsumrelem  10828  fsumiun  10833  isumshft  10846  zsupcllemstep  11023  infssuzex  11027  bezoutlemmain  11069  bj-nntrans  11492
  Copyright terms: Public domain W3C validator