Theorem ffnafv 30077

Description: A function maps to a class to which all values belong, analogous to ffnfv 5869. (Contributed by Alexander van der Vekens, 25-May-2017.)

Assertion

Ref	Expression
ffnafv	|- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F''' x ) e. B ) )

Distinct variable groups:   x, A   x, B   x, F

Proof of Theorem ffnafv

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ffn 5559	. . 3 |- ( F : A --> B -> F Fn A )
2		fafvelrn 30076	. . . 4 |- ( ( F : A --> B /\ x e. A ) -> ( F''' x ) e. B )
3	2	ralrimiva 2799	. . 3 |- ( F : A --> B -> A. x e. A ( F''' x ) e. B )
4	1, 3	jca 532	. 2 |- ( F : A --> B -> ( F Fn A /\ A. x e. A ( F''' x ) e. B ) )
5		simpl 457	. . 3 |- ( ( F Fn A /\ A. x e. A ( F''' x ) e. B ) -> F Fn A )
6		afvelrnb0 30070	. . . . 5 |- ( F Fn A -> ( y e. ran F -> E. x e. A ( F''' x ) = y ) )
7		nfra1 2766	. . . . . 6 |- F/ x A. x e. A ( F''' x ) e. B
8		nfv 1673	. . . . . 6 |- F/ x y e. B
9		rsp 2776	. . . . . . 7 |- ( A. x e. A ( F''' x ) e. B -> ( x e. A -> ( F''' x ) e. B ) )
10		eleq1 2503	. . . . . . . 8 |- ( ( F''' x ) = y -> ( ( F''' x ) e. B <-> y e. B ) )
11	10	biimpcd 224	. . . . . . 7 |- ( ( F''' x ) e. B -> ( ( F''' x ) = y -> y e. B ) )
12	9, 11	syl6 33	. . . . . 6 |- ( A. x e. A ( F''' x ) e. B -> ( x e. A -> ( ( F''' x ) = y -> y e. B ) ) )
13	7, 8, 12	rexlimd 2838	. . . . 5 |- ( A. x e. A ( F''' x ) e. B -> ( E. x e. A ( F''' x ) = y -> y e. B ) )
14	6, 13	sylan9 657	. . . 4 |- ( ( F Fn A /\ A. x e. A ( F''' x ) e. B ) -> ( y e. ran F -> y e. B ) )
15	14	ssrdv 3362	. . 3 |- ( ( F Fn A /\ A. x e. A ( F''' x ) e. B ) -> ran F C_ B )
16		df-f 5422	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
17	5, 15, 16	sylanbrc 664	. 2 |- ( ( F Fn A /\ A. x e. A ( F''' x ) e. B ) -> F : A --> B )
18	4, 17	impbii 188	1 |- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F''' x ) e. B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   A.wral 2715   E.wrex 2716   C_ wss 3328   ran crn 4841   Fn wfn 5413   -->wf 5414  '''cafv 30018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-fv 5426  df-dfat 30020  df-afv 30021

This theorem is referenced by:  ffnaov  30105