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

Metamath Proof Explorer

Theorem eusv2nf

Description: Two ways to express single-valuedness of a class expression A ( x ) . (Contributed by Mario Carneiro, 18-Nov-2016)

Ref Expression
Hypothesis eusv2.1 ⊢ 𝐴 ∈ V
Assertion eusv2nf ( ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 ↔ Ⅎ 𝑥 𝐴 )

Proof

Step Hyp Ref Expression
1 eusv2.1 ⊢ 𝐴 ∈ V
2 nfeu1 ⊢ Ⅎ 𝑦 ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴
3 nfe1 ⊢ Ⅎ 𝑥 ∃ 𝑥 𝑦 = 𝐴
4 3 nfeuw ⊢ Ⅎ 𝑥 ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴
5 1 isseti ⊢ ∃ 𝑦 𝑦 = 𝐴
6 19.8a ⊢ ( 𝑦 = 𝐴 → ∃ 𝑥 𝑦 = 𝐴 )
7 6 ancri ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴 ) )
8 5 7 eximii ⊢ ∃ 𝑦 ( ∃ 𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴 )
9 eupick ⊢ ( ( ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 ∧ ∃ 𝑦 ( ∃ 𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴 ) ) → ( ∃ 𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴 ) )
10 8 9 mpan2 ⊢ ( ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 → ( ∃ 𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴 ) )
11 4 10 alrimi ⊢ ( ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 → ∀ 𝑥 ( ∃ 𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴 ) )
12 nf6 ⊢ ( Ⅎ 𝑥 𝑦 = 𝐴 ↔ ∀ 𝑥 ( ∃ 𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴 ) )
13 11 12 sylibr ⊢ ( ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 → Ⅎ 𝑥 𝑦 = 𝐴 )
14 2 13 alrimi ⊢ ( ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 → ∀ 𝑦 Ⅎ 𝑥 𝑦 = 𝐴 )
15 dfnfc2 ⊢ ( ∀ 𝑥 𝐴 ∈ V → ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 = 𝐴 ) )
16 15 1 mpg ⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 = 𝐴 )
17 14 16 sylibr ⊢ ( ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 → Ⅎ 𝑥 𝐴 )
18 eusvnfb ⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 ↔ ( Ⅎ 𝑥 𝐴 ∧ 𝐴 ∈ V ) )
19 1 18 mpbiran2 ⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 ↔ Ⅎ 𝑥 𝐴 )
20 eusv2i ⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 → ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 )
21 19 20 sylbir ⊢ ( Ⅎ 𝑥 𝐴 → ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 )
22 17 21 impbii ⊢ ( ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 ↔ Ⅎ 𝑥 𝐴 )