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

Theorem cbval 1924
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 198 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
51, 2, 4cbv3 1922 . 2  |-  ( A. x ph  ->  A. y ps )
63biimprd 214 . . . 4  |-  ( x  =  y  ->  ( ps  ->  ph ) )
76equcoms 1651 . . 3  |-  ( y  =  x  ->  ( ps  ->  ph ) )
82, 1, 7cbv3 1922 . 2  |-  ( A. y ps  ->  A. x ph )
95, 8impbii 180 1  |-  ( A. x ph  <->  A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527   F/wnf 1531
This theorem is referenced by:  cbvex  1925  cbvalv  1942  cbval2  1944  sb8eu  2161  abbi  2393  cleqf  2443  cbvralf  2758  ralab2  2930  cbvralcsf  3143  dfss2f  3171  elintab  3873  reusv2lem4  4538  cbviota  5224  sb8iota  5226  dffun6f  5269  findcard2  7098  aceq1  7744  aomclem6  27156  stoweidlem34  27783  stoweidlem59  27808  bnj1385  28865  bnj1476  28879
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator