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

Theorem cbval 1983
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 200 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
51, 2, 4cbv3 1972 . 2  |-  ( A. x ph  ->  A. y ps )
63biimprd 216 . . . 4  |-  ( x  =  y  ->  ( ps  ->  ph ) )
76equcoms 1694 . . 3  |-  ( y  =  x  ->  ( ps  ->  ph ) )
82, 1, 7cbv3 1972 . 2  |-  ( A. y ps  ->  A. x ph )
95, 8impbii 182 1  |-  ( A. x ph  <->  A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550   F/wnf 1554
This theorem is referenced by:  cbvex  1984  cbvalv  1985  cbval2  1990  cbval2OLD  1991  sb8  2170  sb8eu  2301  abbi  2548  cleqf  2598  cbvralf  2928  ralab2  3101  cbvralcsf  3313  dfss2f  3341  elintab  4063  reusv2lem4  4729  cbviota  5425  sb8iota  5427  dffun6f  5470  findcard2  7350  aceq1  8000  aomclem6  27136  stoweidlem34  27761  bnj1385  29266  bnj1476  29280
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator