Description: Obsolete version of elhf as of 27-Sep-2026. (Contributed by Scott Fenton, 9-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elhfOLD | |- ( 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 | r111 | |- R1 : On -1-1-> _V |
|
| 4 | f1fun | |- ( R1 : On -1-1-> _V -> Fun R1 ) |
|
| 5 | eluniima | |- ( Fun R1 -> ( A e. U. ( R1 " _om ) <-> E. x e. _om A e. ( R1 ` x ) ) ) |
|
| 6 | 3 4 5 | mp2b | |- ( A e. U. ( R1 " _om ) <-> E. x e. _om A e. ( R1 ` x ) ) |
| 7 | 2 6 | bitri | |- ( A e. HF <-> E. x e. _om A e. ( R1 ` x ) ) |