This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 | ψ