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

Theorem cbval 1987
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 13-May-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 207 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
51, 2, 4cbv3 1977 . 2  |-  ( A. x ph  ->  A. y ps )
63biimprd 223 . . . 4  |-  ( x  =  y  ->  ( ps  ->  ph ) )
76equcoms 1739 . . 3  |-  ( y  =  x  ->  ( ps  ->  ph ) )
82, 1, 7cbv3 1977 . 2  |-  ( A. y ps  ->  A. x ph )
95, 8impbii 188 1  |-  ( A. x ph  <->  A. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1372   F/wnf 1594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595
This theorem is referenced by:  cbvex  1988  cbvalv  1989  cbval2  1993  sb8  2140  sb8eu  2307  sb8euOLD  2308  sb8euOLDOLD  2309  cleqh  2575  abbiOLD  2592  cleqfOLD  2650  cbvralf  3075  ralab2  3261  cbvralcsf  3460  dfss2f  3488  elintab  4286  reusv2lem4  4644  cbviota  5547  sb8iota  5549  dffun6f  5593  findcard2  7749  aceq1  8487  sbcalf  30107  alrimii  30114  aomclem6  30598  stoweidlem34  31289  bnj1385  32845  bnj1476  32859
  Copyright terms: Public domain W3C validator