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

Metamath Proof Explorer

Theorem cbvralvw

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv with a disjoint variable condition, which does not require ax-10 , ax-11 , ax-12 , ax-13 . (Contributed by NM, 28-Jan-1997) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

Ref Expression
Hypothesis cbvralvw.1 
|- ( x = y -> ( ph <-> ps ) )
Assertion cbvralvw 
|- ( A. x e. A ph <-> A. y e. A ps )

Proof

Step Hyp Ref Expression
1 cbvralvw.1 
 |-  ( x = y -> ( ph <-> ps ) )
2 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
3 2 1 imbi12d 
 |-  ( x = y -> ( ( x e. A -> ph ) <-> ( y e. A -> ps ) ) )
4 3 cbvalvw 
 |-  ( A. x ( x e. A -> ph ) <-> A. y ( y e. A -> ps ) )
5 df-ral 
 |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
6 df-ral 
 |-  ( A. y e. A ps <-> A. y ( y e. A -> ps ) )
7 4 5 6 3bitr4i 
 |-  ( A. x e. A ph <-> A. y e. A ps )