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

Metamath Proof Explorer

Theorem cbv3v

Description: Rule used to change bound variables, using implicit substitution. Version of cbv3 with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 5-Aug-1993) (Revised by BJ, 31-May-2019)

Ref Expression
Hypotheses cbv3v.nf1 
|- F/ y ph
cbv3v.nf2 
|- F/ x ps
cbv3v.1 
|- ( x = y -> ( ph -> ps ) )
Assertion cbv3v 
|- ( A. x ph -> A. y ps )

Proof

Step Hyp Ref Expression
1 cbv3v.nf1 
 |-  F/ y ph
2 cbv3v.nf2 
 |-  F/ x ps
3 cbv3v.1 
 |-  ( x = y -> ( ph -> ps ) )
4 1 nf5ri 
 |-  ( ph -> A. y ph )
5 4 hbal 
 |-  ( A. x ph -> A. y A. x ph )
6 2 3 spimfv 
 |-  ( A. x ph -> ps )
7 5 6 alrimih 
 |-  ( A. x ph -> A. y ps )