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 ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 ↔ ( Ⅎ 𝑥 𝐴 ∧ 𝐴 ∈ V ) )

Proof

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