Theorem dfnfc2

Description: An alternative statement of the effective freeness of a class A , when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016) (Proof shortened by JJ, 26-Jul-2021)

	Ref	Expression
Assertion	dfnfc2	⊢ ( ∀ 𝑥 𝐴 ∈ 𝑉 → ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		nfcvd	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝑦 )
2		id	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝐴 )
3	1 2	nfeqd	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝑦 = 𝐴 )
4	3	alrimiv	⊢ ( Ⅎ 𝑥 𝐴 → ∀ 𝑦 Ⅎ 𝑥 𝑦 = 𝐴 )
5		df-nfc	⊢ ( Ⅎ 𝑥 { 𝐴 } ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ { 𝐴 } )
6		velsn	⊢ ( 𝑦 ∈ { 𝐴 } ↔ 𝑦 = 𝐴 )
7	6	nfbii	⊢ ( Ⅎ 𝑥 𝑦 ∈ { 𝐴 } ↔ Ⅎ 𝑥 𝑦 = 𝐴 )
8	7	albii	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ { 𝐴 } ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 = 𝐴 )
9	5 8	sylbbr	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝑦 = 𝐴 → Ⅎ 𝑥 { 𝐴 } )
10	9	nfunid	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝑦 = 𝐴 → Ⅎ 𝑥 ∪ { 𝐴 } )
11		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 𝐴 ∈ 𝑉
12		unisng	⊢ ( 𝐴 ∈ 𝑉 → ∪ { 𝐴 } = 𝐴 )
13	12	sps	⊢ ( ∀ 𝑥 𝐴 ∈ 𝑉 → ∪ { 𝐴 } = 𝐴 )
14	11 13	nfceqdf	⊢ ( ∀ 𝑥 𝐴 ∈ 𝑉 → ( Ⅎ 𝑥 ∪ { 𝐴 } ↔ Ⅎ 𝑥 𝐴 ) )
15	10 14	imbitrid	⊢ ( ∀ 𝑥 𝐴 ∈ 𝑉 → ( ∀ 𝑦 Ⅎ 𝑥 𝑦 = 𝐴 → Ⅎ 𝑥 𝐴 ) )
16	4 15	impbid2	⊢ ( ∀ 𝑥 𝐴 ∈ 𝑉 → ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 = 𝐴 ) )