Metamath Proof Explorer


Theorem cbv1

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . See cbv1v with disjoint variable conditions, not depending on ax-13 . (Contributed by NM, 5-Aug-1993) (Revised by Mario Carneiro, 3-Oct-2016) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018) (New usage is discouraged.)

Ref Expression
Hypotheses cbv1.1
|- F/ x ph
cbv1.2
|- F/ y ph
cbv1.3
|- ( ph -> F/ y ps )
cbv1.4
|- ( ph -> F/ x ch )
cbv1.5
|- ( ph -> ( x = y -> ( ps -> ch ) ) )
Assertion cbv1
|- ( ph -> ( A. x ps -> A. y ch ) )

Proof

Step Hyp Ref Expression
1 cbv1.1
 |-  F/ x ph
2 cbv1.2
 |-  F/ y ph
3 cbv1.3
 |-  ( ph -> F/ y ps )
4 cbv1.4
 |-  ( ph -> F/ x ch )
5 cbv1.5
 |-  ( ph -> ( x = y -> ( ps -> ch ) ) )
6 2 3 nfim1
 |-  F/ y ( ph -> ps )
7 1 4 nfim1
 |-  F/ x ( ph -> ch )
8 5 com12
 |-  ( x = y -> ( ph -> ( ps -> ch ) ) )
9 8 a2d
 |-  ( x = y -> ( ( ph -> ps ) -> ( ph -> ch ) ) )
10 6 7 9 cbv3
 |-  ( A. x ( ph -> ps ) -> A. y ( ph -> ch ) )
11 1 19.21
 |-  ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
12 2 19.21
 |-  ( A. y ( ph -> ch ) <-> ( ph -> A. y ch ) )
13 10 11 12 3imtr3i
 |-  ( ( ph -> A. x ps ) -> ( ph -> A. y ch ) )
14 13 pm2.86i
 |-  ( ph -> ( A. x ps -> A. y ch ) )