Theorem isfappb ≪ | index | src | ≫

theorem isfappb (F: set) (a b: nat):
  $ isfun F -> (a, b e. F <-> a e. Dom F /\ F @ a = b) $;

Step	Hyp	Ref	Expression
1		preldm	a, b e. F -> a e. Dom F
2	1	anwr	isfun F /\ a, b e. F -> a e. Dom F
3		anl	isfun F /\ a, b e. F -> isfun F
4		anr	isfun F /\ a, b e. F -> a, b e. F
5	3, 4	isfappd	isfun F /\ a, b e. F -> F @ a = b
6	2, 5	iand	isfun F /\ a, b e. F -> a e. Dom F /\ F @ a = b
7		eldm	a e. Dom F <-> E. a1 a, a1 e. F
8		anrl	isfun F /\ (a e. Dom F /\ F @ a = b) -> a e. Dom F
9	7, 8	sylib	isfun F /\ (a e. Dom F /\ F @ a = b) -> E. a1 a, a1 e. F
10		anll	isfun F /\ (a e. Dom F /\ F @ a = b) /\ a, a1 e. F -> isfun F
11		anr	isfun F /\ (a e. Dom F /\ F @ a = b) /\ a, a1 e. F -> a, a1 e. F
12	10, 11	isfappd	isfun F /\ (a e. Dom F /\ F @ a = b) /\ a, a1 e. F -> F @ a = a1
13		anrr	isfun F /\ (a e. Dom F /\ F @ a = b) -> F @ a = b
14	13	anwl	isfun F /\ (a e. Dom F /\ F @ a = b) /\ a, a1 e. F -> F @ a = b
15	12, 14	eqtr3d	isfun F /\ (a e. Dom F /\ F @ a = b) /\ a, a1 e. F -> a1 = b
16	15	preq2d	isfun F /\ (a e. Dom F /\ F @ a = b) /\ a, a1 e. F -> a, a1 = a, b
17	16	eleq1d	isfun F /\ (a e. Dom F /\ F @ a = b) /\ a, a1 e. F -> (a, a1 e. F <-> a, b e. F)
18	17, 11	mpbid	isfun F /\ (a e. Dom F /\ F @ a = b) /\ a, a1 e. F -> a, b e. F
19	18	eexda	isfun F /\ (a e. Dom F /\ F @ a = b) -> E. a1 a, a1 e. F -> a, b e. F
20	9, 19	mpd	isfun F /\ (a e. Dom F /\ F @ a = b) -> a, b e. F
21	6, 20	ibida	isfun F -> (a, b e. F <-> a e. Dom F /\ F @ a = b)

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)