Theorem ffnfv 6042

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 5721	. . 3 |- ( F : A --> B -> F Fn A )
2		ffvelrn 6014	. . . 4 |- ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
3	2	ralrimiva 2857	. . 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 5905	. . . . . 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 2824	. . . . . 6 |- F/ x A. x e. A ( F ` x ) e. B
9		nfv 1694	. . . . . 6 |- F/ x y e. B
10		rsp 2809	. . . . . . 7 |- ( A. x e. A ( F ` x ) e. B -> ( x e. A -> ( F ` x ) e. B ) )
11		eleq1 2515	. . . . . . . 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 2927	. . . . 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 3495	. . 3 |- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ran F C_ B )
17		df-f 5582	. . 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 1383   e. wcel 1804   A.wral 2793   E.wrex 2794   C_ wss 3461   ran crn 4990   Fn wfn 5573   -->wf 5574   ` cfv 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-fv 5586

This theorem is referenced by:  ffnfvf  6043  fnfvrnss  6044  fmpt2d  6046  fconstfv  6118  ffnov  6391  seqomlem2  7118  elixpconst  7479  elixpsn  7510  unblem4  7777  ordtypelem4  7949  oismo  7968  cantnfvalf  8087  rankf  8215  alephon  8453  alephf1  8469  alephf1ALT  8487  alephfplem4  8491  cfsmolem  8653  infpssrlem3  8688  axcc4  8822  domtriomlem  8825  axdclem2  8903  pwfseqlem3  9041  gch3  9057  inar1  9156  peano5nni  10546  cnref1o  11225  seqf2  12107  hashkf  12388  ccatrn  12587  shftf  12893  sqrtf  13177  isercoll2  13472  eff2  13815  reeff1  13836  1arith  14426  ramcl  14528  xpscf  14944  dmaf  15354  cdaf  15355  coapm  15376  odf  16539  gsumpt  16966  gsumptOLD  16967  dprdff  17024  dprdfcntz  17027  dprdffOLD  17030  dprdfcntzOLD  17033  dprdfadd  17038  dprdfaddOLD  17045  dprdlub  17051  mgpf  17188  prdscrngd  17240  isabvd  17447  psrbagcon  18000  subrgmvrf  18102  mplbas2  18112  mplbas2OLD  18113  mvrf2  18135  psgnghm  18593  frlmsslsp  18806  frlmsslspOLD  18807  kqf  20225  fmf  20423  tmdgsum2  20572  prdstmdd  20599  prdstgpd  20600  prdsxmslem2  21009  metdsre  21334  evth  21436  evthicc2  21849  ovolfsf  21860  ovolf  21870  vitalilem2  21995  vitalilem5  21998  0plef  22056  mbfi1fseqlem4  22102  xrge0f  22115  itg2addlem  22142  dvfre  22331  dvne0  22389  mdegxrf  22445  mtest  22775  psercn  22797  recosf1o  22898  logcn  23004  amgm  23296  emcllem7  23307  dchrfi  23506  dchr1re  23514  dchrisum0re  23674  padicabvf  23792  hlimf  26131  pjrni  26596  pjmf1  26610  subfacp1lem3  28603  mrsubrn  28850  msrf  28879  mclsind  28907  neibastop2lem  30153  rrncmslem  30303  hbtlem7  31049  dgraaf  31072  deg1mhm  31143  resincncf  31584  bnj149  33666  cdlemk56  36437