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

Theorem cbvald 1987
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2074. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.)
Hypotheses
Ref Expression
cbvald.1  |-  F/ y
ph
cbvald.2  |-  ( ph  ->  F/ y ps )
cbvald.3  |-  ( ph  ->  ( x  =  y  ->  ( ps  <->  ch )
) )
Assertion
Ref Expression
cbvald  |-  ( ph  ->  ( A. x ps  <->  A. y ch ) )
Distinct variable groups:    ph, x    ch, x
Allowed substitution hints:    ph( y)    ps( x, y)    ch( y)

Proof of Theorem cbvald
StepHypRef Expression
1 nfv 1630 . 2  |-  F/ x ph
2 cbvald.1 . 2  |-  F/ y
ph
3 cbvald.2 . 2  |-  ( ph  ->  F/ y ps )
4 nfv 1630 . . 3  |-  F/ x ch
54a1i 11 . 2  |-  ( ph  ->  F/ x ch )
6 cbvald.3 . 2  |-  ( ph  ->  ( x  =  y  ->  ( ps  <->  ch )
) )
71, 2, 3, 5, 6cbv2 1981 1  |-  ( ph  ->  ( A. x ps  <->  A. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550   F/wnf 1554
This theorem is referenced by:  cbvexd  1989  cbvaldva  1995  axextnd  8471  axrepndlem1  8472  axunndlem1  8475  axpowndlem2  8478  axpowndlem3  8479  axpowndlem4  8480  axregndlem2  8483  axregnd  8484  axinfnd  8486  axacndlem5  8491  axacnd  8492  axextdist  25432  distel  25436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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