Theorem ffnfv 6060

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 5742	. . 3 |- ( F : A --> B -> F Fn A )
2		ffvelrn 6031	. . . 4 |- ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
3	2	ralrimiva 2839	. . 3 |- ( F : A --> B -> A. x e. A ( F ` x ) e. B )
4	1, 3	jca 534	. 2 |- ( F : A --> B -> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
5		simpl 458	. . 3 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F Fn A )
6		fvelrnb 5924	. . . . . 6 |- ( F Fn A -> ( y e. ran F <-> E. x e. A ( F ` x ) = y ) )
7	6	biimpd 210	. . . . 5 |- ( F Fn A -> ( y e. ran F -> E. x e. A ( F ` x ) = y ) )
8		nfra1 2806	. . . . . 6 |- F/ x A. x e. A ( F ` x ) e. B
9		nfv 1751	. . . . . 6 |- F/ x y e. B
10		rsp 2791	. . . . . . 7 |- ( A. x e. A ( F ` x ) e. B -> ( x e. A -> ( F ` x ) e. B ) )
11		eleq1 2494	. . . . . . . 8 |- ( ( F ` x ) = y -> ( ( F ` x ) e. B <-> y e. B ) )
12	11	biimpcd 227	. . . . . . 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 2909	. . . . 5 |- ( A. x e. A ( F ` x ) e. B -> ( E. x e. A ( F ` x ) = y -> y e. B ) )
15	7, 14	sylan9 661	. . . 4 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ( y e. ran F -> y e. B ) )
16	15	ssrdv 3470	. . 3 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ran F C_ B )
17		df-f 5601	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
18	5, 16, 17	sylanbrc 668	. 2 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F : A --> B )
19	4, 18	impbii 190	1 |- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1868   A.wral 2775   E.wrex 2776   C_ wss 3436   ran crn 4850   Fn wfn 5592   -->wf 5593   ` cfv 5597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pr 4656

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-fv 5605

This theorem is referenced by:  ffnfvf  6061  fnfvrnss  6062  fmpt2d  6064  fconstfv  6137  ffnov  6410  seqomlem2  7172  elixpconst  7534  elixpsn  7565  unblem4  7828  ordtypelem4  8038  oismo  8057  cantnfvalf  8171  rankf  8266  alephon  8500  alephf1  8516  alephf1ALT  8534  alephfplem4  8538  cfsmolem  8700  infpssrlem3  8735  axcc4  8869  domtriomlem  8872  axdclem2  8950  pwfseqlem3  9085  gch3  9101  inar1  9200  peano5nni  10612  cnref1o  11297  seqf2  12231  hashkf  12516  ccatrn  12725  shftf  13130  sqrtf  13414  isercoll2  13719  eff2  14140  reeff1  14161  1arith  14858  ramcl  14974  xpscf  15459  dmaf  15931  cdaf  15932  coapm  15953  odf  17173  odfOLD  17189  gsumpt  17581  dprdff  17632  dprdfcntz  17635  dprdfadd  17640  dprdlub  17646  mgpf  17779  prdscrngd  17828  isabvd  18035  psrbagcon  18582  subrgmvrf  18673  mplbas2  18681  mvrf2  18702  psgnghm  19134  frlmsslsp  19340  kqf  20748  fmf  20946  tmdgsum2  21097  prdstmdd  21124  prdstgpd  21125  prdsxmslem2  21530  metdsre  21856  metdsreOLD  21871  evth  21973  evthicc2  22397  ovolfsf  22410  ovolf  22421  vitalilem2  22553  vitalilem5  22556  0plef  22616  mbfi1fseqlem4  22662  xrge0f  22675  itg2addlem  22702  dvfre  22891  dvne0  22949  mdegxrf  23003  mtest  23345  psercn  23367  recosf1o  23470  logcn  23578  amgm  23902  emcllem7  23913  dchrfi  24169  dchr1re  24177  dchrisum0re  24337  padicabvf  24455  hlimf  26875  pjrni  27340  pjmf1  27354  bnj149  29681  subfacp1lem3  29900  mrsubrn  30146  msrf  30175  mclsind  30203  neibastop2lem  31008  rrncmslem  32077  cdlemk56  34456  hbtlem7  35903  dgraaf  35930  dgraafOLD  35931  deg1mhm  36003  resincncf  37571  dvnprodlem1  37640  fge0iccico  37999  elhoi  38138  ovnsubaddlem1  38166