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

Theorem cbvald 2044
Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2052. (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 1770 . . 3  |-  ( ph  ->  A. y ph )
32alrimiv 1638 . 2  |-  ( ph  ->  A. x A. y ph )
4 cbvald.2 . . 3  |-  ( ph  ->  F/ y ps )
5 nfvd 1627 . . 3  |-  ( ph  ->  F/ x ch )
6 cbvald.3 . . 3  |-  ( ph  ->  ( x  =  y  ->  ( ps  <->  ch )
) )
74, 5, 6cbv2 2021 . 2  |-  ( A. x A. y ph  ->  ( A. x ps  <->  A. y ch ) )
83, 7syl 16 1  |-  ( ph  ->  ( A. x ps  <->  A. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546   F/wnf 1550
This theorem is referenced by:  cbvexd  2045  cbvaldva  2046  axextnd  8401  axrepndlem1  8402  axunndlem1  8405  axpowndlem2  8408  axpowndlem3  8409  axpowndlem4  8410  axregndlem2  8413  axregnd  8414  axinfnd  8416  axacndlem5  8421  axacnd  8422  axextdist  25182  distel  25186
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator