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

Metamath Proof Explorer

Theorem eusvnfb

Description: Two ways to say that A ( x ) is a set expression that does not depend on x . (Contributed by Mario Carneiro, 18-Nov-2016)

Ref Expression
Assertion eusvnfb ⊢ ∃! y ∀ x y = A ↔ Ⅎ _ x A ∧ A ∈ V

Proof

Step Hyp Ref Expression
1 eusvnf ⊢ ∃! y ∀ x y = A → Ⅎ _ x A
2 euex ⊢ ∃! y ∀ x y = A → ∃ y ∀ x y = A
3 eqvisset ⊢ y = A → A ∈ V
4 3 sps ⊢ ∀ x y = A → A ∈ V
5 4 exlimiv ⊢ ∃ y ∀ x y = A → A ∈ V
6 2 5 syl ⊢ ∃! y ∀ x y = A → A ∈ V
7 1 6 jca ⊢ ∃! y ∀ x y = A → Ⅎ _ x A ∧ A ∈ V
8 isset ⊢ A ∈ V ↔ ∃ y y = A
9 nfcvd ⊢ Ⅎ _ x A → Ⅎ _ x y
10 id ⊢ Ⅎ _ x A → Ⅎ _ x A
11 9 10 nfeqd ⊢ Ⅎ _ x A → Ⅎ x y = A
12 11 nf5rd ⊢ Ⅎ _ x A → y = A → ∀ x y = A
13 12 eximdv ⊢ Ⅎ _ x A → ∃ y y = A → ∃ y ∀ x y = A
14 8 13 biimtrid ⊢ Ⅎ _ x A → A ∈ V → ∃ y ∀ x y = A
15 14 imp ⊢ Ⅎ _ x A ∧ A ∈ V → ∃ y ∀ x y = A
16 eusv1 ⊢ ∃! y ∀ x y = A ↔ ∃ y ∀ x y = A
17 15 16 sylibr ⊢ Ⅎ _ x A ∧ A ∈ V → ∃! y ∀ x y = A
18 7 17 impbii ⊢ ∃! y ∀ x y = A ↔ Ⅎ _ x A ∧ A ∈ V