Theorem ffnfv 6038

Description: A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.)

Assertion

Ref	Expression
ffnfv	|- ( 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 ffnfv

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ffn 5722	. . 3 |- ( F : A --> B -> F Fn A )
2		ffvelrn 6010	. . . 4 |- ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
3	2	ralrimiva 2871	. . 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		fvelrnb 5906	. . . . . 6 |- ( F Fn A -> ( y e. ran F <-> E. x e. A ( F ` x ) = y ) )
7	6	biimpd 207	. . . . 5 |- ( F Fn A -> ( y e. ran F -> E. x e. A ( F ` x ) = y ) )
8		nfra1 2838	. . . . . 6 |- F/ x A. x e. A ( F ` x ) e. B
9		nfv 1678	. . . . . 6 |- F/ x y e. B
10		rsp 2823	. . . . . . 7 |- ( A. x e. A ( F ` x ) e. B -> ( x e. A -> ( F ` x ) e. B ) )
11		eleq1 2532	. . . . . . . 8 |- ( ( F ` x ) = y -> ( ( F ` x ) e. B <-> y e. B ) )
12	11	biimpcd 224	. . . . . . 7 |- ( ( F ` x ) e. B -> ( ( F ` x ) = y -> y e. B ) )
13	10, 12	syl6 33	. . . . . 6 |- ( A. x e. A ( F ` x ) e. B -> ( x e. A -> ( ( F ` x ) = y -> y e. B ) ) )
14	8, 9, 13	rexlimd 2940	. . . . 5 |- ( A. x e. A ( F ` x ) e. B -> ( E. x e. A ( F ` x ) = y -> y e. B ) )
15	7, 14	sylan9 657	. . . 4 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ( y e. ran F -> y e. B ) )
16	15	ssrdv 3503	. . 3 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ran F C_ B )
17		df-f 5583	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
18	5, 16, 17	sylanbrc 664	. 2 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F : A --> B )
19	4, 18	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 1374   e. wcel 1762   A.wral 2807   E.wrex 2808   C_ wss 3469   ran crn 4993   Fn wfn 5574   -->wf 5575   ` cfv 5579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-fv 5587

This theorem is referenced by:  ffnfvf  6039  fnfvrnss  6040  fmpt2d  6042  ffnov  6381  seqomlem2  7106  elixpconst  7467  elixpsn  7498  unblem4  7764  ordtypelem4  7935  oismo  7954  cantnfvalf  8073  rankf  8201  alephon  8439  alephf1  8455  alephf1ALT  8473  alephfplem4  8477  cfsmolem  8639  infpssrlem3  8674  axcc4  8808  domtriomlem  8811  axdclem2  8889  pwfseqlem3  9027  gch3  9043  inar1  9142  peano5nni  10528  cnref1o  11204  seqf2  12082  hashkf  12362  shftf  12862  sqrf  13145  isercoll2  13440  eff2  13684  reeff1  13705  1arith  14293  ramcl  14395  xpscf  14810  dmaf  15223  cdaf  15224  coapm  15245  odf  16350  gsumpt  16772  gsumptOLD  16773  dprdff  16829  dprdfcntz  16832  dprdffOLD  16835  dprdfcntzOLD  16838  dprdfadd  16843  dprdfaddOLD  16850  dprdlub  16856  mgpf  16990  prdscrngd  17039  isabvd  17245  psrbagcon  17786  subrgmvrf  17888  mplbas2  17898  mplbas2OLD  17899  mvrf2  17921  psgnghm  18376  frlmsslsp  18589  frlmsslspOLD  18590  kqf  19976  fmf  20174  tmdgsum2  20323  prdstmdd  20350  prdstgpd  20351  prdsxmslem2  20760  metdsre  21085  evth  21187  evthicc2  21600  ovolfsf  21611  ovolf  21621  vitalilem2  21746  vitalilem5  21749  0plef  21807  mbfi1fseqlem4  21853  xrge0f  21866  itg2addlem  21893  dvfre  22082  dvne0  22140  mdegxrf  22196  mtest  22526  psercn  22548  recosf1o  22648  logcn  22749  amgm  23041  emcllem7  23052  dchrfi  23251  dchr1re  23259  dchrisum0re  23419  padicabvf  23537  hlimf  25817  pjrni  26282  pjmf1  26296  subfacp1lem3  28252  neibastop2lem  29768  rrncmslem  29918  hbtlem7  30667  dgraaf  30690  deg1mhm  30761  resincncf  31168  bnj149  32887  cdlemk56  35642