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

Theorem cbval 1712
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)
Hypotheses
Ref Expression
cbval.1  |-  F/ y
ph
cbval.2  |-  F/ x ps
cbval.3  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbval  |-  ( A. x ph  <->  A. y ps )

Proof of Theorem cbval
StepHypRef Expression
1 cbval.1 . . 3  |-  F/ y
ph
21nfri 1484 . 2  |-  ( ph  ->  A. y ph )
3 cbval.2 . . 3  |-  F/ x ps
43nfri 1484 . 2  |-  ( ps 
->  A. x ps )
5 cbval.3 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
62, 4, 5cbvalh 1711 1  |-  ( A. x ph  <->  A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   A.wal 1314   F/wnf 1421
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 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-nf 1422
This theorem is referenced by:  sb8  1812  cbval2  1873  sb8eu  1990  abbi  2231  cleqf  2282  cbvralf  2625  ralab2  2821  cbvralcsf  3032  dfss2f  3058  elintab  3752  cbviota  5063  sb8iota  5065  dffun6f  5106  dffun4f  5109  mptfvex  5474  findcard2  6751  findcard2s  6752
  Copyright terms: Public domain W3C validator