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

Theorem cbval 1969
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 1959 . 2  |-  ( A. x ph  ->  A. y ps )
63biimprd 223 . . . 4  |-  ( x  =  y  ->  ( ps  ->  ph ) )
76equcoms 1733 . . 3  |-  ( y  =  x  ->  ( ps  ->  ph ) )
82, 1, 7cbv3 1959 . 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 1367   F/wnf 1589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590
This theorem is referenced by:  cbvex  1970  cbvalv  1971  cbval2  1975  sb8  2124  sb8eu  2292  sb8euOLD  2293  sb8euOLDOLD  2294  abbi  2551  cleqf  2601  cbvralf  2939  ralab2  3122  cbvralcsf  3317  dfss2f  3345  elintab  4137  reusv2lem4  4494  cbviota  5384  sb8iota  5386  dffun6f  5430  findcard2  7550  aceq1  8285  sbcalf  28917  alrimii  28924  aomclem6  29409  stoweidlem34  29826  bnj1385  31823  bnj1476  31837
  Copyright terms: Public domain W3C validator