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 ψ χ
cbvralv2.2 x = y A = B
Assertion cbvralv2 x A ψ y B χ

Proof

Step Hyp Ref Expression
1 cbvralv2.1 x = y ψ χ
2 cbvralv2.2 x = y A = B
3 nfcv _ y A
4 nfcv _ x B
5 nfv y ψ
6 nfv x χ
7 3 4 5 6 2 1 cbvralcsf x A ψ y B χ