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

Theorem cbval 2026
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 2020 . 2  |-  ( A. x ph  ->  A. y ps )
63biimprd 223 . . . 4  |-  ( x  =  y  ->  ( ps  ->  ph ) )
76equcoms 1800 . . 3  |-  ( y  =  x  ->  ( ps  ->  ph ) )
82, 1, 7cbv3 2020 . 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 1396   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622
This theorem is referenced by:  cbvex  2027  cbvalv  2028  cbval2  2032  sb8  2169  sb8eu  2319  sb8euOLD  2320  cleqh  2569  abbiOLD  2586  cleqfOLD  2644  cbvralf  3075  ralab2  3261  cbvralcsf  3452  dfss2f  3480  elintab  4282  reusv2lem4  4641  cbviota  5539  sb8iota  5541  dffun6f  5584  findcard2  7752  aceq1  8489  sbcalf  30757  alrimii  30764  aomclem6  31244  stoweidlem34  32055  bnj1385  34292  bnj1476  34306
  Copyright terms: Public domain W3C validator