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|yxφ

Proof

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