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

Theorem cbvald 2026
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2080. (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 1708 . 2  |-  F/ x ph
2 cbvald.1 . 2  |-  F/ y
ph
3 cbvald.2 . 2  |-  ( ph  ->  F/ y ps )
4 nfvd 1709 . 2  |-  ( ph  ->  F/ x ch )
5 cbvald.3 . 2  |-  ( ph  ->  ( x  =  y  ->  ( ps  <->  ch )
) )
61, 2, 3, 4, 5cbv2 2021 1  |-  ( ph  ->  ( A. x ps  <->  A. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1393   F/wnf 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-nf 1618
This theorem is referenced by:  cbvexd  2027  cbvaldva  2033  axextnd  8983  axrepndlem1  8984  axunndlem1  8987  axpowndlem2  8990  axpowndlem2OLD  8991  axpowndlem3  8992  axpowndlem3OLD  8993  axpowndlem4  8994  axregndlem2  8997  axregnd  8998  axregndOLD  8999  axinfnd  9001  axacndlem5  9006  axacnd  9007  axextdist  29449  distel  29453  wl-sb8eut  30227
  Copyright terms: Public domain W3C validator