Theorem ffnfv 3904

Description: A function maps to a class to which all values belong.

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

Step	Hyp	Ref	Expression
1		ffn 3702	. . 3 |- (F:A-->B -> F Fn A)
2		ffvelrn 3890	. . . 4 |- ((F:A-->B /\ x e. A) -> (F` x) e. B)
3	2	r19.21aiva 1752	. . 3 |- (F:A-->B -> A.x e. A (F` x) e. B)
4	1, 3	jca 286	. 2 |- (F:A-->B -> (F Fn A /\ A.x e. A (F` x) e. B))
5		pm3.26 317	. . . 4 |- ((F Fn A /\ A.x e. A (F` x) e. B) -> F Fn A)
6		fvelrnb 3836	. . . . . . . 8 |- (F Fn A -> (y e. ran F <-> E.x e. A (F` x) = y))
7	6	biimpd 151	. . . . . . 7 |- (F Fn A -> (y e. ran F -> E.x e. A (F` x) = y))
8		hbra1 1725	. . . . . . . 8 |- (A.x e. A (F` x) e. B -> A.xA.x e. A (F` x) e. B)
9		ax-17 1003	. . . . . . . 8 |- (y e. B -> A.x y e. B)
10		ra4 1732	. . . . . . . . 9 |- (A.x e. A (F` x) e. B -> (x e. A -> (F` x) e. B))
11		eleq1 1571	. . . . . . . . . 10 |- ((F` x) = y -> ((F` x) e. B <-> y e. B))
12	11	biimpcd 153	. . . . . . . . 9 |- ((F` x) e. B -> ((F` x) = y -> y e. B))
13	10, 12	syl6 22	. . . . . . . 8 |- (A.x e. A (F` x) e. B -> (x e. A -> ((F` x) = y -> y e. B)))
14	8, 9, 13	r19.23ad 1783	. . . . . . 7 |- (A.x e. A (F` x) e. B -> (E.x e. A (F` x) = y -> y e. B))
15	7, 14	sylan9 470	. . . . . 6 |- ((F Fn A /\ A.x e. A (F` x) e. B) -> (y e. ran F -> y e. B))
16	15	r19.21aiv 1751	. . . . 5 |- ((F Fn A /\ A.x e. A (F` x) e. B) -> A.y e. ran F y e. B)
17		dfss3 2103	. . . . 5 |- (ran F (_ B <-> A.y e. ran F y e. B)
18	16, 17	sylibr 198	. . . 4 |- ((F Fn A /\ A.x e. A (F` x) e. B) -> ran F (_ B)
19	5, 18	jca 286	. . 3 |- ((F Fn A /\ A.x e. A (F` x) e. B) -> (F Fn A /\ ran F (_ B))
20		df-f 3249	. . 3 |- (F:A-->B <-> (F Fn A /\ ran F (_ B))
21	19, 20	sylibr 198	. 2 |- ((F Fn A /\ A.x e. A (F` x) e. B) -> F:A-->B)
22	4, 21	impbii 155	1 |- (F:A-->B <-> (F Fn A /\ A.x e. A (F` x) e. B))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221   = wceq 988   e. wcel 990  A.wral 1683  E.wrex 1684   (_ wss 2091  ran crn 3226   Fn wfn 3232  -->wf 3233  ` cfv 3237

This theorem is referenced by:  ffnfvf 3905  fnfvrnss 3906  fopabfv 3907  abianfp 4038  ffnoprval 4091  elixpconst 4438  mapixp 4449  mapxpen 4584  unblem4 4630  alephfplem4 4988  ser1refi 6625  ser1f2i 6627  shftf 6644  ser0fi 6688  ref 6882  imf 6883  caurei 7050  cauimi 7051  ser1absdiflem 7052  serzrefi 7174  caucvg3ai 7287  caucvg3lem 7289  cvgcmp2lem 7303  cvgcmp2clem 7305  cvgcmp3ci 7309  eff 7436  eff2 7493  sinf 7564  cosf 7565  ubthlem6 8653  htthlem11 8749  efif 8840  pjmf1 9781

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832  ax-un 2920

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-ral 1687  df-rex 1688  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-id 2889  df-xp 3239  df-cnv 3241  df-co 3242  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fun 3247  df-fn 3248  df-f 3249  df-fv 3253

Copyright terms: Public domain