theorem preldm (A: set) (a b: nat): $ a, b e. A -> a e. Dom A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eldm | a e. Dom A <-> E. y a, y e. A |
|
| 2 | preq2 | y = b -> a, y = a, b |
|
| 3 | 2 | eleq1d | y = b -> (a, y e. A <-> a, b e. A) |
| 4 | 3 | iexe | a, b e. A -> E. y a, y e. A |
| 5 | 1, 4 | sylibr | a, b e. A -> a e. Dom A |