This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvaldw

Description: Deduction used to change bound variables, using implicit substitution. Version of cbvald with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 2-Jan-2002) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 cbvaldw.1 
 |-  F/ y ph
2 cbvaldw.2 
 |-  ( ph -> F/ y ps )
3 cbvaldw.3 
 |-  ( ph -> ( x = y -> ( ps <-> ch ) ) )
4 nfv 
 |-  F/ x ph
5 nfvd 
 |-  ( ph -> F/ x ch )
6 4 1 2 5 3 cbv2w 
 |-  ( ph -> ( A. x ps <-> A. y ch ) )