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

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 ( ∀ 𝑥 𝐴 ∈ 𝑉 → ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 = 𝐴 ) )

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 ⊢ ( ∀ 𝑥 𝐴 ∈ 𝑉 → ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 = 𝐴 ) )