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

Metamath Proof Explorer

Theorem sb8iota

Description: Variable substitution in description binder. Compare sb8eu . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 18-Mar-2013) (New usage is discouraged.)

Ref Expression
Hypothesis sb8iota.1 ⊢ Ⅎ y φ
Assertion sb8iota ⊢ ι x | φ = ι y | y x φ

Proof

Step Hyp Ref Expression
1 sb8iota.1 ⊢ Ⅎ y φ
2 nfv ⊢ Ⅎ w φ ↔ x = z
3 2 sb8 ⊢ ∀ x φ ↔ x = z ↔ ∀ w w x φ ↔ x = z
4 sbbi ⊢ w x φ ↔ x = z ↔ w x φ ↔ w x x = z
5 1 nfsb ⊢ Ⅎ y w x φ
6 equsb3 ⊢ w x x = z ↔ w = z
7 nfv ⊢ Ⅎ y w = z
8 6 7 nfxfr ⊢ Ⅎ y w x x = z
9 5 8 nfbi ⊢ Ⅎ y w x φ ↔ w x x = z
10 4 9 nfxfr ⊢ Ⅎ y w x φ ↔ x = z
11 nfv ⊢ Ⅎ w y x φ ↔ x = z
12 sbequ ⊢ w = y → w x φ ↔ x = z ↔ y x φ ↔ x = z
13 10 11 12 cbvalv1 ⊢ ∀ w w x φ ↔ x = z ↔ ∀ y y x φ ↔ x = z
14 equsb3 ⊢ y x x = z ↔ y = z
15 14 sblbis ⊢ y x φ ↔ x = z ↔ y x φ ↔ y = z
16 15 albii ⊢ ∀ y y x φ ↔ x = z ↔ ∀ y y x φ ↔ y = z
17 3 13 16 3bitri ⊢ ∀ x φ ↔ x = z ↔ ∀ y y x φ ↔ y = z
18 17 abbii ⊢ z | ∀ x φ ↔ x = z = z | ∀ y y x φ ↔ y = z
19 18 unieqi ⊢ ⋃ z | ∀ x φ ↔ x = z = ⋃ z | ∀ y y x φ ↔ y = z
20 dfiota2 ⊢ ι x | φ = ⋃ z | ∀ x φ ↔ x = z
21 dfiota2 ⊢ ι y | y x φ = ⋃ z | ∀ y y x φ ↔ y = z
22 19 20 21 3eqtr4i ⊢ ι x | φ = ι y | y x φ