Theorem ffnfv 6033

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 5713	. . 3 |- ( F : A --> B -> F Fn A )
2		ffvelrn 6005	. . . 4 |- ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
3	2	ralrimiva 2868	. . 3 |- ( F : A --> B -> A. x e. A ( F ` x ) e. B )
4	1, 3	jca 530	. 2 |- ( F : A --> B -> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
5		simpl 455	. . 3 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F Fn A )
6		fvelrnb 5895	. . . . . 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 2835	. . . . . 6 |- F/ x A. x e. A ( F ` x ) e. B
9		nfv 1712	. . . . . 6 |- F/ x y e. B
10		rsp 2820	. . . . . . 7 |- ( A. x e. A ( F ` x ) e. B -> ( x e. A -> ( F ` x ) e. B ) )
11		eleq1 2526	. . . . . . . 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 2938	. . . . 5 |- ( A. x e. A ( F ` x ) e. B -> ( E. x e. A ( F ` x ) = y -> y e. B ) )
15	7, 14	sylan9 655	. . . 4 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ( y e. ran F -> y e. B ) )
16	15	ssrdv 3495	. . 3 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ran F C_ B )
17		df-f 5574	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
18	5, 16, 17	sylanbrc 662	. 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 367   = wceq 1398   e. wcel 1823   A.wral 2804   E.wrex 2805   C_ wss 3461   ran crn 4989   Fn wfn 5565   -->wf 5566   ` cfv 5570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-fv 5578

This theorem is referenced by:  ffnfvf  6034  fnfvrnss  6035  fmpt2d  6037  fconstfv  6108  ffnov  6379  seqomlem2  7108  elixpconst  7470  elixpsn  7501  unblem4  7767  ordtypelem4  7938  oismo  7957  cantnfvalf  8075  rankf  8203  alephon  8441  alephf1  8457  alephf1ALT  8475  alephfplem4  8479  cfsmolem  8641  infpssrlem3  8676  axcc4  8810  domtriomlem  8813  axdclem2  8891  pwfseqlem3  9027  gch3  9043  inar1  9142  peano5nni  10534  cnref1o  11216  seqf2  12111  hashkf  12392  ccatrn  12598  shftf  12997  sqrtf  13281  isercoll2  13576  eff2  13919  reeff1  13940  1arith  14532  ramcl  14634  xpscf  15058  dmaf  15530  cdaf  15531  coapm  15552  odf  16763  gsumpt  17187  gsumptOLD  17188  dprdff  17244  dprdfcntz  17247  dprdffOLD  17250  dprdfcntzOLD  17253  dprdfadd  17258  dprdfaddOLD  17265  dprdlub  17271  mgpf  17408  prdscrngd  17460  isabvd  17667  psrbagcon  18220  subrgmvrf  18322  mplbas2  18332  mplbas2OLD  18333  mvrf2  18355  psgnghm  18792  frlmsslsp  19001  kqf  20417  fmf  20615  tmdgsum2  20764  prdstmdd  20791  prdstgpd  20792  prdsxmslem2  21201  metdsre  21526  evth  21628  evthicc2  22041  ovolfsf  22052  ovolf  22062  vitalilem2  22187  vitalilem5  22190  0plef  22248  mbfi1fseqlem4  22294  xrge0f  22307  itg2addlem  22334  dvfre  22523  dvne0  22581  mdegxrf  22637  mtest  22968  psercn  22990  recosf1o  23091  logcn  23199  amgm  23521  emcllem7  23532  dchrfi  23731  dchr1re  23739  dchrisum0re  23899  padicabvf  24017  hlimf  26356  pjrni  26821  pjmf1  26835  subfacp1lem3  28893  mrsubrn  29140  msrf  29169  mclsind  29197  neibastop2lem  30421  rrncmslem  30571  hbtlem7  31318  dgraaf  31340  deg1mhm  31411  resincncf  31919  dvnprodlem1  31985  bnj149  34353  cdlemk56  37113