Metamath Proof Explorer


Theorem cbviota

Description: Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbviotaw when possible. (Contributed by Andrew Salmon, 1-Aug-2011) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbviota.1 x = y φ ψ
2 cbviota.2 y φ
3 cbviota.3 x ψ
4 nfv z φ x = w
5 nfs1v x z x φ
6 nfv x z = w
7 5 6 nfbi x z x φ z = w
8 sbequ12 x = z φ z x φ
9 equequ1 x = z x = w z = w
10 8 9 bibi12d x = z φ x = w z x φ z = w
11 4 7 10 cbvalv1 x φ x = w z z x φ z = w
12 2 nfsb y z x φ
13 nfv y z = w
14 12 13 nfbi y z x φ z = w
15 nfv z ψ y = w
16 sbequ z = y z x φ y x φ
17 3 1 sbie y x φ ψ
18 16 17 bitrdi z = y z x φ ψ
19 equequ1 z = y z = w y = w
20 18 19 bibi12d z = y z x φ z = w ψ y = w
21 14 15 20 cbvalv1 z z x φ z = w y ψ y = w
22 11 21 bitri x φ x = w y ψ y = w
23 22 abbii w | x φ x = w = w | y ψ y = w
24 23 unieqi w | x φ x = w = w | y ψ y = w
25 dfiota2 ι x | φ = w | x φ x = w
26 dfiota2 ι y | ψ = w | y ψ y = w
27 24 25 26 3eqtr4i ι x | φ = ι y | ψ