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

Theorem cbvald 1998
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2052. (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 1683 . 2  |-  F/ x ph
2 cbvald.1 . 2  |-  F/ y
ph
3 cbvald.2 . 2  |-  ( ph  ->  F/ y ps )
4 nfv 1683 . . 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 1992 1  |-  ( ph  ->  ( A. x ps  <->  A. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1377   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600
This theorem is referenced by:  cbvexd  1999  cbvaldva  2005  axextnd  8967  axrepndlem1  8968  axunndlem1  8971  axpowndlem2  8974  axpowndlem2OLD  8975  axpowndlem3  8976  axpowndlem3OLD  8977  axpowndlem4  8978  axregndlem2  8981  axregnd  8982  axregndOLD  8983  axinfnd  8985  axacndlem5  8990  axacnd  8991  axextdist  29085  distel  29089  wl-sb8eut  29875
  Copyright terms: Public domain W3C validator