# 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 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\}={A}$

### Proof

Step Hyp Ref Expression
1 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\to {z}\in {A}$
2 nfcr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
3 2 nf5rd ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left({z}\in {A}\to \forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right)$
4 1 3 impbid2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}↔{z}\in {A}\right)$
5 4 abbi1dv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\}={A}$