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	⊢ ( ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 ↔ Ⅎ 𝑥 𝐴 )