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

Theorem cbvald 1961
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 1969. (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 1754 . . 3  |-  ( ph  ->  A. y ph )
32alrimiv 1621 . 2  |-  ( ph  ->  A. x A. y ph )
4 cbvald.2 . . 3  |-  ( ph  ->  F/ y ps )
5 nfvd 1610 . . 3  |-  ( ph  ->  F/ x ch )
6 cbvald.3 . . 3  |-  ( ph  ->  ( x  =  y  ->  ( ps  <->  ch )
) )
74, 5, 6cbv2 1934 . 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 1530   F/wnf 1534
This theorem is referenced by:  cbvexd  1962  cbvaldva  1963  axextnd  8229  axrepndlem1  8230  axunndlem1  8233  axpowndlem2  8236  axpowndlem3  8237  axpowndlem4  8238  axregndlem2  8241  axregnd  8242  axinfnd  8244  axacndlem5  8249  axacnd  8250  axextdist  24227  distel  24231
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator