Theorem ffnfv 5867

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 5557	. . 3 |- ( F : A --> B -> F Fn A )
2		ffvelrn 5839	. . . 4 |- ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
3	2	ralrimiva 2797	. . 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 5737	. . . . . 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 2764	. . . . . 6 |- F/ x A. x e. A ( F ` x ) e. B
9		nfv 1673	. . . . . 6 |- F/ x y e. B
10		rsp 2774	. . . . . . 7 |- ( A. x e. A ( F ` x ) e. B -> ( x e. A -> ( F ` x ) e. B ) )
11		eleq1 2501	. . . . . . . 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 2836	. . . . 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 3360	. . 3 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ran F C_ B )
17		df-f 5420	. . 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 1369   e. wcel 1756   A.wral 2713   E.wrex 2714   C_ wss 3326   ran crn 4839   Fn wfn 5411   -->wf 5412   ` cfv 5416

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 2422  ax-sep 4411  ax-nul 4419  ax-pr 4529

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 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3185  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-nul 3636  df-if 3790  df-sn 3876  df-pr 3878  df-op 3882  df-uni 4090  df-br 4291  df-opab 4349  df-mpt 4350  df-id 4634  df-xp 4844  df-rel 4845  df-cnv 4846  df-co 4847  df-dm 4848  df-rn 4849  df-iota 5379  df-fun 5418  df-fn 5419  df-f 5420  df-fv 5424

This theorem is referenced by:  ffnfvf  5868  fnfvrnss  5869  fmpt2d  5871  ffnov  6192  seqomlem2  6904  elixpconst  7269  elixpsn  7300  unblem4  7565  ordtypelem4  7733  oismo  7752  cantnfvalf  7871  rankf  7999  alephon  8237  alephf1  8253  alephf1ALT  8271  alephfplem4  8275  cfsmolem  8437  infpssrlem3  8472  axcc4  8606  domtriomlem  8609  axdclem2  8687  pwfseqlem3  8825  gch3  8841  inar1  8940  peano5nni  10323  cnref1o  10984  seqf2  11823  hashkf  12103  shftf  12566  sqrf  12849  isercoll2  13144  eff2  13381  reeff1  13402  1arith  13986  ramcl  14088  xpscf  14502  dmaf  14915  cdaf  14916  coapm  14937  odf  16038  gsumpt  16452  gsumptOLD  16453  dprdff  16494  dprdfcntz  16497  dprdffOLD  16500  dprdfcntzOLD  16503  dprdfadd  16508  dprdfaddOLD  16515  dprdlub  16521  mgpf  16654  prdscrngd  16703  isabvd  16903  psrbagcon  17438  subrgmvrf  17539  mplbas2  17549  mplbas2OLD  17550  mvrf2  17572  psgnghm  18008  frlmsslsp  18221  frlmsslspOLD  18222  kqf  19318  fmf  19516  tmdgsum2  19665  prdstmdd  19692  prdstgpd  19693  prdsxmslem2  20102  metdsre  20427  evth  20529  evthicc2  20942  ovolfsf  20953  ovolf  20963  vitalilem2  21087  vitalilem5  21090  0plef  21148  mbfi1fseqlem4  21194  xrge0f  21207  itg2addlem  21234  dvfre  21423  dvne0  21481  mdegxrf  21537  mtest  21867  psercn  21889  recosf1o  21989  logcn  22090  amgm  22382  emcllem7  22393  dchrfi  22592  dchr1re  22600  dchrisum0re  22760  padicabvf  22878  hlimf  24638  pjrni  25103  pjmf1  25117  subfacp1lem3  27068  neibastop2lem  28578  rrncmslem  28728  hbtlem7  29478  dgraaf  29501  deg1mhm  29572  bnj149  31865  cdlemk56  34612