Theorem appelrn | index | src |

theorem appelrn (F: set) (a: nat): $ isfun F -> a e. Dom F -> F @ a e. Ran F $;
StepHypRefExpression
1 eldm
a e. Dom F <-> E. a1 a, a1 e. F
2 anl
isfun F /\ a, a1 e. F -> isfun F
3 anr
isfun F /\ a, a1 e. F -> a, a1 e. F
4 2, 3 isfappd
isfun F /\ a, a1 e. F -> F @ a = a1
5 4 eleq1d
isfun F /\ a, a1 e. F -> (F @ a e. Ran F <-> a1 e. Ran F)
6 prelrn
a, a1 e. F -> a1 e. Ran F
7 6 anwr
isfun F /\ a, a1 e. F -> a1 e. Ran F
8 5, 7 mpbird
isfun F /\ a, a1 e. F -> F @ a e. Ran F
9 8 eexda
isfun F -> E. a1 a, a1 e. F -> F @ a e. Ran F
10 1, 9 syl5bi
isfun F -> a e. Dom F -> F @ a e. Ran F

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano2, addeq, muleq)