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

Metamath Proof Explorer

Theorem cbvalv1

Description: Rule used to change bound variables, using implicit substitution. Version of cbval with a disjoint variable condition, which does not require ax-13 . See cbvalvw for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv for another variant. (Contributed by NM, 13-May-1993) (Revised by BJ, 31-May-2019)

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

Proof

Step Hyp Ref Expression
1 cbvalv1.nf1 
 |-  F/ y ph
2 cbvalv1.nf2 
 |-  F/ x ps
3 cbvalv1.1 
 |-  ( x = y -> ( ph <-> ps ) )
4 3 biimpd 
 |-  ( x = y -> ( ph -> ps ) )
5 1 2 4 cbv3v 
 |-  ( A. x ph -> A. y ps )
6 3 biimprd 
 |-  ( x = y -> ( ps -> ph ) )
7 6 equcoms 
 |-  ( y = x -> ( ps -> ph ) )
8 2 1 7 cbv3v 
 |-  ( A. y ps -> A. x ph )
9 5 8 impbii 
 |-  ( A. x ph <-> A. y ps )