Metamath Proof Explorer

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 ⊢ ∀ x A ∈ V → Ⅎ _ x A ↔ ∀ y Ⅎ x y = A

Proof

Step Hyp Ref Expression
1 nfcvd ⊢ Ⅎ _ x A → Ⅎ _ x y
2 id ⊢ Ⅎ _ x A → Ⅎ _ x A
3 1 2 nfeqd ⊢ Ⅎ _ x A → Ⅎ x y = A
4 3 alrimiv ⊢ Ⅎ _ x A → ∀ y Ⅎ x y = A
5 df-nfc ⊢ Ⅎ _ x A ↔ ∀ y Ⅎ x y ∈ A
6 velsn ⊢ y ∈ A ↔ y = A
7 6 nfbii ⊢ Ⅎ x y ∈ A ↔ Ⅎ x y = A
8 7 albii ⊢ ∀ y Ⅎ x y ∈ A ↔ ∀ y Ⅎ x y = A
9 5 8 sylbbr ⊢ ∀ y Ⅎ x y = A → Ⅎ _ x A
10 9 nfunid ⊢ ∀ y Ⅎ x y = A → Ⅎ _ x ⋃ A
11 nfa1 ⊢ Ⅎ x ∀ x A ∈ V
12 unisng ⊢ A ∈ V → ⋃ A = A
13 12 sps ⊢ ∀ x A ∈ V → ⋃ A = A
14 11 13 nfceqdf ⊢ ∀ x A ∈ V → Ⅎ _ x ⋃ A ↔ Ⅎ _ x A
15 10 14 syl5ib ⊢ ∀ x A ∈ V → ∀ y Ⅎ x y = A → Ⅎ _ x A
16 4 15 impbid2 ⊢ ∀ x A ∈ V → Ⅎ _ x A ↔ ∀ y Ⅎ x y = A