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 ) )