MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbval Unicode version

Theorem cbval 1937
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
2 cbval.2 . . 3  |-  F/ x ps
3 cbval.3 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
43biimpd 198 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
51, 2, 4cbv3 1935 . 2  |-  ( A. x ph  ->  A. y ps )
63biimprd 214 . . . 4  |-  ( x  =  y  ->  ( ps  ->  ph ) )
76equcoms 1666 . . 3  |-  ( y  =  x  ->  ( ps  ->  ph ) )
82, 1, 7cbv3 1935 . 2  |-  ( A. y ps  ->  A. x ph )
95, 8impbii 180 1  |-  ( A. x ph  <->  A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530   F/wnf 1534
This theorem is referenced by:  cbvex  1938  cbvalv  1955  cbval2  1957  sb8eu  2174  abbi  2406  cleqf  2456  cbvralf  2771  ralab2  2943  cbvralcsf  3156  dfss2f  3184  elintab  3889  reusv2lem4  4554  cbviota  5240  sb8iota  5242  dffun6f  5285  findcard2  7114  aceq1  7760  aomclem6  27259  stoweidlem34  27886  stoweidlem59  27911  bnj1385  29181  bnj1476  29195
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator