Metamath Proof Explorer


Theorem cbvralw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvral with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 31-Jul-2003) (Revised by Gino Giotto, 10-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 cbvralw.1
 |-  F/ y ph
2 cbvralw.2
 |-  F/ x ps
3 cbvralw.3
 |-  ( x = y -> ( ph <-> ps ) )
4 nfcv
 |-  F/_ x A
5 nfcv
 |-  F/_ y A
6 4 5 1 2 3 cbvralfw
 |-  ( A. x e. A ph <-> A. y e. A ps )