Theorem dffun7 3481

Description: Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun6 3480.

Assertion

Ref	Expression
dffun7	|- (Fun A <-> (Rel A /\ A.x e. dom AE!y xAy))

Distinct variable group:   x,y,A

Proof of Theorem dffun7

Step	Hyp	Ref	Expression
1		funrel 3474	. . 3 |- (Fun A -> Rel A)
2		ax-17 1190	. . . . . 6 |- (Fun A -> A.yFun A)
3		hbeu1 1365	. . . . . 6 |- (E!y<.x, y>. e. A -> A.yE!y<.x, y>. e. A)
4		funeu2 3479	. . . . . . 7 |- ((Fun A /\ <.x, y>. e. A) -> E!y<.x, y>. e. A)
5	4	ex 373	. . . . . 6 |- (Fun A -> (<.x, y>. e. A -> E!y<.x, y>. e. A))
6	2, 3, 5	19.23ad 1042	. . . . 5 |- (Fun A -> (E.y<.x, y>. e. A -> E!y<.x, y>. e. A))
7		visset 1788	. . . . . 6 |- x e. V
8	7	eldm2 3265	. . . . 5 |- (x e. dom A <-> E.y<.x, y>. e. A)
9		df-br 2588	. . . . . 6 |- (xAy <-> <.x, y>. e. A)
10	9	eubii 1364	. . . . 5 |- (E!y xAy <-> E!y<.x, y>. e. A)
11	6, 8, 10	3imtr4g 551	. . . 4 |- (Fun A -> (x e. dom A -> E!y xAy))
12	11	r19.21aiv 1689	. . 3 |- (Fun A -> A.x e. dom AE!y xAy)
13	1, 12	jca 288	. 2 |- (Fun A -> (Rel A /\ A.x e. dom AE!y xAy))
14		eumo 1388	. . . . 5 |- (E!y xAy -> E*y xAy)
15	14	r19.20si 1682	. . . 4 |- (A.x e. dom AE!y xAy -> A.x e. dom AE*y xAy)
16	15	anim2i 335	. . 3 |- ((Rel A /\ A.x e. dom AE!y xAy) -> (Rel A /\ A.x e. dom AE*y xAy))
17		dffun6 3480	. . 3 |- (Fun A <-> (Rel A /\ A.x e. dom AE*y xAy))
18	16, 17	sylibr 200	. 2 |- ((Rel A /\ A.x e. dom AE!y xAy) -> Fun A)
19	13, 18	impbi 157	1 |- (Fun A <-> (Rel A /\ A.x e. dom AE!y xAy))

Syntax hints:   <-> wb 146   /\ wa 223  E.wex 956   e. wcel 1105  E!weu 1357  E*wmo 1358  A.wral 1621  <.cop 2382   class class class wbr 2587  dom cdm 3133  Rel wrel 3138  Fun wfun 3139

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-pow 2710  ax-pr 2747

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-op 2387  df-br 2588  df-opab 2635  df-id 2797  df-cnv 3149  df-co 3150  df-dm 3151  df-fun 3155

Copyright terms: Public domain