Theorem ffnfv 6057

Description: A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.)

Assertion

Ref	Expression
ffnfv

Distinct variable groups:   ,   ,   ,

Proof of Theorem ffnfv

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ffn 5736	. . 3
2		ffvelrn 6029	. . . 4
3	2	ralrimiva 2871	. . 3
4	1, 3	jca 532	. 2
5		simpl 457	. . 3
6		fvelrnb 5920	. . . . . 6
7	6	biimpd 207	. . . . 5
8		nfra1 2838	. . . . . 6
9		nfv 1707	. . . . . 6
10		rsp 2823	. . . . . . 7
11		eleq1 2529	. . . . . . . 8
12	11	biimpcd 224	. . . . . . 7
13	10, 12	syl6 33	. . . . . 6
14	8, 9, 13	rexlimd 2941	. . . . 5
15	7, 14	sylan9 657	. . . 4
16	15	ssrdv 3509	. . 3
17		df-f 5597	. . 3
18	5, 16, 17	sylanbrc 664	. 2
19	4, 18	impbii 188	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807  E.wrex 2808  C_wss 3475  rancrn 5005  Fnwfn 5588  -->wf 5589  `cfv 5593

This theorem is referenced by:  ffnfvf  6058  fnfvrnss  6059  fmpt2d  6061  fconstfv  6133  ffnov  6406  seqomlem2  7135  elixpconst  7497  elixpsn  7528  unblem4  7795  ordtypelem4  7967  oismo  7986  cantnfvalf  8105  rankf  8233  alephon  8471  alephf1  8487  alephf1ALT  8505  alephfplem4  8509  cfsmolem  8671  infpssrlem3  8706  axcc4  8840  domtriomlem  8843  axdclem2  8921  pwfseqlem3  9059  gch3  9075  inar1  9174  peano5nni  10564  cnref1o  11244  seqf2  12126  hashkf  12407  ccatrn  12606  shftf  12912  sqrtf  13196  isercoll2  13491  eff2  13834  reeff1  13855  1arith  14445  ramcl  14547  xpscf  14963  dmaf  15376  cdaf  15377  coapm  15398  odf  16561  gsumpt  16988  gsumptOLD  16989  dprdff  17046  dprdfcntz  17049  dprdffOLD  17052  dprdfcntzOLD  17055  dprdfadd  17060  dprdfaddOLD  17067  dprdlub  17073  mgpf  17210  prdscrngd  17262  isabvd  17469  psrbagcon  18022  subrgmvrf  18124  mplbas2  18134  mplbas2OLD  18135  mvrf2  18157  psgnghm  18616  frlmsslsp  18829  frlmsslspOLD  18830  kqf  20248  fmf  20446  tmdgsum2  20595  prdstmdd  20622  prdstgpd  20623  prdsxmslem2  21032  metdsre  21357  evth  21459  evthicc2  21872  ovolfsf  21883  ovolf  21893  vitalilem2  22018  vitalilem5  22021  0plef  22079  mbfi1fseqlem4  22125  xrge0f  22138  itg2addlem  22165  dvfre  22354  dvne0  22412  mdegxrf  22468  mtest  22799  psercn  22821  recosf1o  22922  logcn  23028  amgm  23320  emcllem7  23331  dchrfi  23530  dchr1re  23538  dchrisum0re  23698  padicabvf  23816  hlimf  26155  pjrni  26620  pjmf1  26634  subfacp1lem3  28626  mrsubrn  28873  msrf  28902  mclsind  28930  neibastop2lem  30178  rrncmslem  30328  hbtlem7  31074  dgraaf  31096  deg1mhm  31167  resincncf  31677  dvnprodlem1  31743  bnj149  33933  cdlemk56  36697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601