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

Theorem cbval 2114
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 212 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
51, 2, 4cbv3 2108 . 2  |-  ( A. x ph  ->  A. y ps )
63biimprd 231 . . . 4  |-  ( x  =  y  ->  ( ps  ->  ph ) )
76equcoms 1867 . . 3  |-  ( y  =  x  ->  ( ps  ->  ph ) )
82, 1, 7cbv3 2108 . 2  |-  ( A. y ps  ->  A. x ph )
95, 8impbii 192 1  |-  ( A. x ph  <->  A. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wal 1445   F/wnf 1670
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1667  df-nf 1671
This theorem is referenced by:  cbvex  2115  cbvalv  2116  cbval2  2120  sb8  2253  sb8eu  2332  cbvralf  2980  ralab2  3170  cbvralcsf  3362  dfss2f  3390  elintab  4214  reusv2lem4  4579  cbviota  5529  sb8iota  5531  dffun6f  5574  findcard2  7797  aceq1  8534  bnj1385  29649  bnj1476  29663  sbcalf  32353  alrimii  32360  aomclem6  35918  rababg  36180  dfcleqf  37426  stoweidlem34  37951
  Copyright terms: Public domain W3C validator