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	⊢ ( Ⅎ 𝑥 𝐴 → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } = 𝐴 )