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

Theorem cbvald 1948
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 1956. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.)
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 cbvald.1 . . . 4  |-  F/ y
ph
21nfri 1742 . . 3  |-  ( ph  ->  A. y ph )
32alrimiv 1617 . 2  |-  ( ph  ->  A. x A. y ph )
4 cbvald.2 . . 3  |-  ( ph  ->  F/ y ps )
5 nfvd 1606 . . 3  |-  ( ph  ->  F/ x ch )
6 cbvald.3 . . 3  |-  ( ph  ->  ( x  =  y  ->  ( ps  <->  ch )
) )
74, 5, 6cbv2 1921 . 2  |-  ( A. x A. y ph  ->  ( A. x ps  <->  A. y ch ) )
83, 7syl 15 1  |-  ( ph  ->  ( A. x ps  <->  A. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527   F/wnf 1531
This theorem is referenced by:  cbvexd  1949  cbvaldva  1950  axextnd  8213  axrepndlem1  8214  axunndlem1  8217  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axregndlem2  8225  axregnd  8226  axinfnd  8228  axacndlem5  8233  axacnd  8234  axextdist  24156  distel  24160
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator