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

Metamath Proof Explorer

Theorem cbvraldva

Description: Rule used to change the bound variable in a restricted universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017) Avoid ax-9 , ax-ext . (Revised by Wolf Lammen, 9-Mar-2025)

Ref Expression
Hypothesis cbvraldva.1 
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
Assertion cbvraldva 
|- ( ph -> ( A. x e. A ps <-> A. y e. A ch ) )

Proof

Step Hyp Ref Expression
1 cbvraldva.1 
 |-  ( ( ph /\ x = y ) -> ( ps <-> ch ) )
2 1 ancoms 
 |-  ( ( x = y /\ ph ) -> ( ps <-> ch ) )
3 2 pm5.74da 
 |-  ( x = y -> ( ( ph -> ps ) <-> ( ph -> ch ) ) )
4 3 cbvralvw 
 |-  ( A. x e. A ( ph -> ps ) <-> A. y e. A ( ph -> ch ) )
5 r19.21v 
 |-  ( A. x e. A ( ph -> ps ) <-> ( ph -> A. x e. A ps ) )
6 r19.21v 
 |-  ( A. y e. A ( ph -> ch ) <-> ( ph -> A. y e. A ch ) )
7 4 5 6 3bitr3i 
 |-  ( ( ph -> A. x e. A ps ) <-> ( ph -> A. y e. A ch ) )
8 7 pm5.74ri 
 |-  ( ph -> ( A. x e. A ps <-> A. y e. A ch ) )