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

Theorem cbval 2005
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 1999 . 2  |-  ( A. x ph  ->  A. y ps )
63biimprd 223 . . . 4  |-  ( x  =  y  ->  ( ps  ->  ph ) )
76equcoms 1779 . . 3  |-  ( y  =  x  ->  ( ps  ->  ph ) )
82, 1, 7cbv3 1999 . 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 1379   F/wnf 1601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-nf 1602
This theorem is referenced by:  cbvex  2006  cbvalv  2007  cbval2  2011  sb8  2151  sb8eu  2302  sb8euOLD  2303  cleqh  2556  abbiOLD  2573  cleqfOLD  2631  cbvralf  3062  ralab2  3248  cbvralcsf  3449  dfss2f  3477  elintab  4278  reusv2lem4  4637  cbviota  5542  sb8iota  5544  dffun6f  5588  findcard2  7758  aceq1  8496  sbcalf  30485  alrimii  30492  aomclem6  30973  stoweidlem34  31701  bnj1385  33598  bnj1476  33612
  Copyright terms: Public domain W3C validator