Metamath Proof Explorer


Theorem cbvriota

Description: Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvriotaw when possible. (Contributed by NM, 18-Mar-2013) (Revised by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses cbvriota.1 y φ
cbvriota.2 x ψ
cbvriota.3 x = y φ ψ
Assertion cbvriota ι x A | φ = ι y A | ψ

Proof

Step Hyp Ref Expression
1 cbvriota.1 y φ
2 cbvriota.2 x ψ
3 cbvriota.3 x = y φ ψ
4 eleq1w x = z x A z A
5 sbequ12 x = z φ z x φ
6 4 5 anbi12d x = z x A φ z A z x φ
7 nfv z x A φ
8 nfv x z A
9 nfs1v x z x φ
10 8 9 nfan x z A z x φ
11 6 7 10 cbviota ι x | x A φ = ι z | z A z x φ
12 eleq1w z = y z A y A
13 sbequ z = y z x φ y x φ
14 2 3 sbie y x φ ψ
15 13 14 bitrdi z = y z x φ ψ
16 12 15 anbi12d z = y z A z x φ y A ψ
17 nfv y z A
18 1 nfsb y z x φ
19 17 18 nfan y z A z x φ
20 nfv z y A ψ
21 16 19 20 cbviota ι z | z A z x φ = ι y | y A ψ
22 11 21 eqtri ι x | x A φ = ι y | y A ψ
23 df-riota ι x A | φ = ι x | x A φ
24 df-riota ι y A | ψ = ι y | y A ψ
25 22 23 24 3eqtr4i ι x A | φ = ι y A | ψ