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

Metamath Proof Explorer

Theorem abidnf

Description: Identity used to create closed-form versions of bound-variable hypothesis builders for class expressions. (Contributed by NM, 10-Nov-2005) (Proof shortened by Mario Carneiro, 12-Oct-2016)

Ref Expression
Assertion abidnf ( Ⅎ 𝑥 𝐴 → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } = 𝐴 )

Proof

Step Hyp Ref Expression
1 sp ⊢ ( ∀ 𝑥 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐴 )
2 nfcr ⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝑧 ∈ 𝐴 )
3 2 nf5rd ⊢ ( Ⅎ 𝑥 𝐴 → ( 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 ) )
4 1 3 impbid2 ⊢ ( Ⅎ 𝑥 𝐴 → ( ∀ 𝑥 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
5 4 eqabcdv ⊢ ( Ⅎ 𝑥 𝐴 → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } = 𝐴 )