Metamath Proof Explorer


Theorem cbvralv2

Description: Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by David Moews, 1-May-2017) (New usage is discouraged.)

Ref Expression
Hypotheses cbvralv2.1
|- ( x = y -> ( ps <-> ch ) )
cbvralv2.2
|- ( x = y -> A = B )
Assertion cbvralv2
|- ( A. x e. A ps <-> A. y e. B ch )

Proof

Step Hyp Ref Expression
1 cbvralv2.1
 |-  ( x = y -> ( ps <-> ch ) )
2 cbvralv2.2
 |-  ( x = y -> A = B )
3 nfcv
 |-  F/_ y A
4 nfcv
 |-  F/_ x B
5 nfv
 |-  F/ y ps
6 nfv
 |-  F/ x ch
7 3 4 5 6 2 1 cbvralcsf
 |-  ( A. x e. A ps <-> A. y e. B ch )