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

Metamath Proof Explorer

Theorem eusvnf

Description: Even if x is free in A , it is effectively bound when A ( x ) is single-valued. (Contributed by NM, 14-Oct-2010) (Revised by Mario Carneiro, 14-Oct-2016)

Ref Expression
Assertion eusvnf ⊢ ∃! y ∀ x y = A → Ⅎ _ x A

Proof

Step Hyp Ref Expression
1 euex ⊢ ∃! y ∀ x y = A → ∃ y ∀ x y = A
2 nfcv ⊢ Ⅎ _ x z
3 nfcsb1v ⊢ Ⅎ _ x ⦋ z / x⦌ A
4 3 nfeq2 ⊢ Ⅎ x y = ⦋ z / x⦌ A
5 csbeq1a ⊢ x = z → A = ⦋ z / x⦌ A
6 5 eqeq2d ⊢ x = z → y = A ↔ y = ⦋ z / x⦌ A
7 2 4 6 spcgf ⊢ z ∈ V → ∀ x y = A → y = ⦋ z / x⦌ A
8 7 elv ⊢ ∀ x y = A → y = ⦋ z / x⦌ A
9 nfcv ⊢ Ⅎ _ x w
10 nfcsb1v ⊢ Ⅎ _ x ⦋ w / x⦌ A
11 10 nfeq2 ⊢ Ⅎ x y = ⦋ w / x⦌ A
12 csbeq1a ⊢ x = w → A = ⦋ w / x⦌ A
13 12 eqeq2d ⊢ x = w → y = A ↔ y = ⦋ w / x⦌ A
14 9 11 13 spcgf ⊢ w ∈ V → ∀ x y = A → y = ⦋ w / x⦌ A
15 14 elv ⊢ ∀ x y = A → y = ⦋ w / x⦌ A
16 8 15 eqtr3d ⊢ ∀ x y = A → ⦋ z / x⦌ A = ⦋ w / x⦌ A
17 16 alrimivv ⊢ ∀ x y = A → ∀ z ∀ w ⦋ z / x⦌ A = ⦋ w / x⦌ A
18 sbnfc2 ⊢ Ⅎ _ x A ↔ ∀ z ∀ w ⦋ z / x⦌ A = ⦋ w / x⦌ A
19 17 18 sylibr ⊢ ∀ x y = A → Ⅎ _ x A
20 19 exlimiv ⊢ ∃ y ∀ x y = A → Ⅎ _ x A
21 1 20 syl ⊢ ∃! y ∀ x y = A → Ⅎ _ x A