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

Theorem cbvald 2129
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2182. (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 1772 . 2  |-  F/ x ph
2 cbvald.1 . 2  |-  F/ y
ph
3 cbvald.2 . 2  |-  ( ph  ->  F/ y ps )
4 nfvd 1773 . 2  |-  ( ph  ->  F/ x ch )
5 cbvald.3 . 2  |-  ( ph  ->  ( x  =  y  ->  ( ps  <->  ch )
) )
61, 2, 3, 4, 5cbv2 2124 1  |-  ( ph  ->  ( A. x ps  <->  A. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wal 1453   F/wnf 1678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-nf 1679
This theorem is referenced by:  cbvexd  2130  cbvaldva  2135  axextnd  9042  axrepndlem1  9043  axunndlem1  9046  axpowndlem2  9049  axpowndlem3  9050  axpowndlem4  9051  axregndlem2  9054  axregnd  9055  axinfnd  9057  axacndlem5  9062  axacnd  9063  axextdist  30495  distel  30499  wl-sb8eut  31951
  Copyright terms: Public domain W3C validator