Description: Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015) Reduce axiom usage and shorten proof. (Revised by BJ, 27-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elhf | |- ( A e. HF <-> E. x e. _om A e. ( R1 ` x ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-hf | |- HF = U. ( R1 " _om ) |
|
| 2 | 1 | eleq2i | |- ( A e. HF <-> A e. U. ( R1 " _om ) ) |
| 3 | r1fun | |- Fun R1 |
|
| 4 | eluniima | |- ( Fun R1 -> ( A e. U. ( R1 " _om ) <-> E. x e. _om A e. ( R1 ` x ) ) ) |
|
| 5 | 3 4 | ax-mp | |- ( A e. U. ( R1 " _om ) <-> E. x e. _om A e. ( R1 ` x ) ) |
| 6 | 2 5 | bitri | |- ( A e. HF <-> E. x e. _om A e. ( R1 ` x ) ) |