Metamath Proof Explorer


Theorem cbvralf

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvralfw when possible. (Contributed by NM, 7-Mar-2004) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses cbvralf.1 _ x A
cbvralf.2 _ y A
cbvralf.3 y φ
cbvralf.4 x ψ
cbvralf.5 x = y φ ψ
Assertion cbvralf x A φ y A ψ

Proof

Step Hyp Ref Expression
1 cbvralf.1 _ x A
2 cbvralf.2 _ y A
3 cbvralf.3 y φ
4 cbvralf.4 x ψ
5 cbvralf.5 x = y φ ψ
6 nfv z x A φ
7 1 nfcri x z A
8 nfs1v x z x φ
9 7 8 nfim x z A z x φ
10 eleq1w x = z x A z A
11 sbequ12 x = z φ z x φ
12 10 11 imbi12d x = z x A φ z A z x φ
13 6 9 12 cbvalv1 x x A φ z z A z x φ
14 2 nfcri y z A
15 3 nfsb y z x φ
16 14 15 nfim y z A z x φ
17 nfv z y A ψ
18 eleq1w z = y z A y A
19 sbequ z = y z x φ y x φ
20 4 5 sbie y x φ ψ
21 19 20 bitrdi z = y z x φ ψ
22 18 21 imbi12d z = y z A z x φ y A ψ
23 16 17 22 cbvalv1 z z A z x φ y y A ψ
24 13 23 bitri x x A φ y y A ψ
25 df-ral x A φ x x A φ
26 df-ral y A ψ y y A ψ
27 24 25 26 3bitr4i x A φ y A ψ