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

Metamath Proof Explorer

Theorem cbviotaw

Description: Change bound variables in a description binder. Version of cbviota with a disjoint variable condition, which does not require ax-13 . (Contributed by Andrew Salmon, 1-Aug-2011) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

Ref Expression
Hypotheses cbviotaw.1 ⊢ x = y → φ ↔ ψ
cbviotaw.2 ⊢ Ⅎ y φ
cbviotaw.3 ⊢ Ⅎ x ψ
Assertion cbviotaw ⊢ ι x | φ = ι y | ψ

Proof

Step Hyp Ref Expression
1 cbviotaw.1 ⊢ x = y → φ ↔ ψ
2 cbviotaw.2 ⊢ Ⅎ y φ
3 cbviotaw.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 nfsbv ⊢ Ⅎ y z x φ
13 nfv ⊢ Ⅎ y z = w
14 12 13 nfbi ⊢ Ⅎ y z x φ ↔ z = w
15 nfv ⊢ Ⅎ z ψ ↔ y = w
16 3 1 sbhypf ⊢ z = y → z x φ ↔ ψ
17 equequ1 ⊢ z = y → z = w ↔ y = w
18 16 17 bibi12d ⊢ z = y → z x φ ↔ z = w ↔ ψ ↔ y = w
19 14 15 18 cbvalv1 ⊢ ∀ z z x φ ↔ z = w ↔ ∀ y ψ ↔ y = w
20 11 19 bitri ⊢ ∀ x φ ↔ x = w ↔ ∀ y ψ ↔ y = w
21 20 abbii ⊢ w | ∀ x φ ↔ x = w = w | ∀ y ψ ↔ y = w
22 21 unieqi ⊢ ⋃ w | ∀ x φ ↔ x = w = ⋃ w | ∀ y ψ ↔ y = w
23 dfiota2 ⊢ ι x | φ = ⋃ w | ∀ x φ ↔ x = w
24 dfiota2 ⊢ ι y | ψ = ⋃ w | ∀ y ψ ↔ y = w
25 22 23 24 3eqtr4i ⊢ ι x | φ = ι y | ψ