Theorem dffun7 3532

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

Assertion

Ref	Expression
dffun7	⊢ (Fun A ↔ (Rel A ⋀ ∀x ∈ dom A∃!y xAy))

Distinct variable group:   x,y,A

Proof of Theorem dffun7

Step	Hyp	Ref	Expression
1		funrel 3525	. . 3 ⊢ (Fun A → Rel A)
2		ax-17 969	. . . . . 6 ⊢ (Fun A → ∀yFun A)
3		hbeu1 1386	. . . . . 6 ⊢ (∃!y⟨x, y⟩ ∈ A → ∀y∃!y⟨x, y⟩ ∈ A)
4		funeu2 3530	. . . . . . 7 ⊢ ((Fun A ⋀ ⟨x, y⟩ ∈ A) → ∃!y⟨x, y⟩ ∈ A)
5	4	ex 373	. . . . . 6 ⊢ (Fun A → (⟨x, y⟩ ∈ A → ∃!y⟨x, y⟩ ∈ A))
6	2, 3, 5	19.23ad 1064	. . . . 5 ⊢ (Fun A → (∃y⟨x, y⟩ ∈ A → ∃!y⟨x, y⟩ ∈ A))
7		visset 1809	. . . . . 6 ⊢ x ∈ V
8	7	eldm2 3303	. . . . 5 ⊢ (x ∈ dom A ↔ ∃y⟨x, y⟩ ∈ A)
9		df-br 2615	. . . . . 6 ⊢ (xAy ↔ ⟨x, y⟩ ∈ A)
10	9	eubii 1385	. . . . 5 ⊢ (∃!y xAy ↔ ∃!y⟨x, y⟩ ∈ A)
11	6, 8, 10	3imtr4g 552	. . . 4 ⊢ (Fun A → (x ∈ dom A → ∃!y xAy))
12	11	r19.21aiv 1710	. . 3 ⊢ (Fun A → ∀x ∈ dom A∃!y xAy)
13	1, 12	jca 288	. 2 ⊢ (Fun A → (Rel A ⋀ ∀x ∈ dom A∃!y xAy))
14		eumo 1409	. . . . 5 ⊢ (∃!y xAy → ∃*y xAy)
15	14	r19.20si 1703	. . . 4 ⊢ (∀x ∈ dom A∃!y xAy → ∀x ∈ dom A∃*y xAy)
16	15	anim2i 335	. . 3 ⊢ ((Rel A ⋀ ∀x ∈ dom A∃!y xAy) → (Rel A ⋀ ∀x ∈ dom A∃*y xAy))
17		dffun6 3531	. . 3 ⊢ (Fun A ↔ (Rel A ⋀ ∀x ∈ dom A∃*y xAy))
18	16, 17	sylibr 200	. 2 ⊢ ((Rel A ⋀ ∀x ∈ dom A∃!y xAy) → Fun A)
19	13, 18	impbi 157	1 ⊢ (Fun A ↔ (Rel A ⋀ ∀x ∈ dom A∃!y xAy))

Syntax hints:   ↔ wb 146   ⋀ wa 223   ∈ wcel 956  ∃wex 978  ∃!weu 1378  ∃*wmo 1379  ∀wral 1642  ⟨cop 2407   class class class wbr 2614  dom cdm 3165  Rel wrel 3170  Fun wfun 3171

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-br 2615  df-opab 2662  df-id 2830  df-cnv 3181  df-co 3182  df-dm 3183  df-fun 3187

Copyright terms: Public domain