Theorem ffnfv 6072

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 5751	. . 3 |- ( F : A --> B -> F Fn A )
2		ffvelrn 6043	. . . 4 |- ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
3	2	ralrimiva 2814	. . 3 |- ( F : A --> B -> A. x e. A ( F ` x ) e. B )
4	1, 3	jca 539	. 2 |- ( F : A --> B -> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
5		simpl 463	. . 3 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F Fn A )
6		fvelrnb 5935	. . . . . 6 |- ( F Fn A -> ( y e. ran F <-> E. x e. A ( F ` x ) = y ) )
7	6	biimpd 212	. . . . 5 |- ( F Fn A -> ( y e. ran F -> E. x e. A ( F ` x ) = y ) )
8		nfra1 2781	. . . . . 6 |- F/ x A. x e. A ( F ` x ) e. B
9		nfv 1772	. . . . . 6 |- F/ x y e. B
10		rsp 2766	. . . . . . 7 |- ( A. x e. A ( F ` x ) e. B -> ( x e. A -> ( F ` x ) e. B ) )
11		eleq1 2528	. . . . . . . 8 |- ( ( F ` x ) = y -> ( ( F ` x ) e. B <-> y e. B ) )
12	11	biimpcd 232	. . . . . . 7 |- ( ( F ` x ) e. B -> ( ( F ` x ) = y -> y e. B ) )
13	10, 12	syl6 34	. . . . . 6 |- ( A. x e. A ( F ` x ) e. B -> ( x e. A -> ( ( F ` x ) = y -> y e. B ) ) )
14	8, 9, 13	rexlimd 2883	. . . . 5 |- ( A. x e. A ( F ` x ) e. B -> ( E. x e. A ( F ` x ) = y -> y e. B ) )
15	7, 14	sylan9 667	. . . 4 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ( y e. ran F -> y e. B ) )
16	15	ssrdv 3450	. . 3 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ran F C_ B )
17		df-f 5605	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
18	5, 16, 17	sylanbrc 675	. 2 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F : A --> B )
19	4, 18	impbii 192	1 |- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1455   e. wcel 1898   A.wral 2749   E.wrex 2750   C_ wss 3416   ran crn 4854   Fn wfn 5596   -->wf 5597   ` cfv 5601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609

This theorem is referenced by:  ffnfvf  6073  fnfvrnss  6074  frnssb  6075  fmpt2d  6077  fconstfv  6151  ffnov  6427  seqomlem2  7194  elixpconst  7556  elixpsn  7587  unblem4  7852  ordtypelem4  8062  oismo  8081  cantnfvalf  8196  rankf  8291  alephon  8526  alephf1  8542  alephf1ALT  8560  alephfplem4  8564  cfsmolem  8726  infpssrlem3  8761  axcc4  8895  domtriomlem  8898  axdclem2  8976  pwfseqlem3  9111  gch3  9127  inar1  9226  peano5nni  10640  cnref1o  11326  seqf2  12264  hashkf  12549  iswrdsymb  12720  ccatrn  12769  shftf  13191  sqrtf  13475  isercoll2  13781  eff2  14202  reeff1  14223  1arith  14920  ramcl  15036  xpscf  15521  dmaf  15993  cdaf  15994  coapm  16015  odf  17235  odfOLD  17251  gsumpt  17643  dprdff  17694  dprdfcntz  17697  dprdfadd  17702  dprdlub  17708  mgpf  17841  prdscrngd  17890  isabvd  18097  psrbagcon  18644  subrgmvrf  18735  mplbas2  18743  mvrf2  18764  psgnghm  19197  frlmsslsp  19403  kqf  20811  fmf  21009  tmdgsum2  21160  prdstmdd  21187  prdstgpd  21188  prdsxmslem2  21593  metdsre  21919  metdsreOLD  21934  evth  22036  evthicc2  22460  ovolfsf  22473  ovolf  22484  vitalilem2  22616  vitalilem5  22619  0plef  22679  mbfi1fseqlem4  22725  xrge0f  22738  itg2addlem  22765  dvfre  22954  dvne0  23012  mdegxrf  23066  mtest  23408  psercn  23430  recosf1o  23533  logcn  23641  amgm  23965  emcllem7  23976  dchrfi  24232  dchr1re  24240  dchrisum0re  24400  padicabvf  24518  hlimf  26939  pjrni  27404  pjmf1  27418  bnj149  29735  subfacp1lem3  29954  mrsubrn  30200  msrf  30229  mclsind  30257  neibastop2lem  31065  rrncmslem  32209  cdlemk56  34583  hbtlem7  36029  dgraaf  36056  dgraafOLD  36057  deg1mhm  36129  resincncf  37790  dvnprodlem1  37859  qndenserrnbllem  38201  fge0iccico  38250  elhoi  38402  ovnsubaddlem1  38430  hoiqssbllem3  38484  vtxdgfisf  39586