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

Theorem cbvald 1985
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2039. (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 1674 . 2  |-  F/ x ph
2 cbvald.1 . 2  |-  F/ y
ph
3 cbvald.2 . 2  |-  ( ph  ->  F/ y ps )
4 nfv 1674 . . 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 1979 1  |-  ( ph  ->  ( A. x ps  <->  A. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1368   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591
This theorem is referenced by:  cbvexd  1986  cbvaldva  1992  axextnd  8869  axrepndlem1  8870  axunndlem1  8873  axpowndlem2  8876  axpowndlem2OLD  8877  axpowndlem3  8878  axpowndlem3OLD  8879  axpowndlem4  8880  axregndlem2  8883  axregnd  8884  axregndOLD  8885  axinfnd  8887  axacndlem5  8892  axacnd  8893  axextdist  27777  distel  27781  wl-sb8eut  28566
  Copyright terms: Public domain W3C validator