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 | |- ( F/_ x A -> { z | A. x z e. A } = A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sp | |- ( A. x z e. A -> z e. A ) |
|
| 2 | nfcr | |- ( F/_ x A -> F/ x z e. A ) |
|
| 3 | 2 | nf5rd | |- ( F/_ x A -> ( z e. A -> A. x z e. A ) ) |
| 4 | 1 3 | impbid2 | |- ( F/_ x A -> ( A. x z e. A <-> z e. A ) ) |
| 5 | 4 | abbi1dv | |- ( F/_ x A -> { z | A. x z e. A } = A ) |