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

Theorem cbvald 1986
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2069. (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 1629 . 2  |-  F/ x ph
2 cbvald.1 . 2  |-  F/ y
ph
3 cbvald.2 . 2  |-  ( ph  ->  F/ y ps )
4 nfv 1629 . . 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 1980 1  |-  ( ph  ->  ( A. x ps  <->  A. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549   F/wnf 1553
This theorem is referenced by:  cbvexd  1988  cbvaldva  1994  axextnd  8458  axrepndlem1  8459  axunndlem1  8462  axpowndlem2  8465  axpowndlem3  8466  axpowndlem4  8467  axregndlem2  8470  axregnd  8471  axinfnd  8473  axacndlem5  8478  axacnd  8479  axextdist  25419  distel  25423
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator