Theorem ffnfv 3819

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 3619	. . 3 |- (F:A-->B -> F Fn A)
2		ffvelrn 3805	. . . 4 |- ((F:A-->B /\ x e. A) -> (F` x) e. B)
3	2	r19.21aiva 1711	. . 3 |- (F:A-->B -> A.x e. A (F` x) e. B)
4	1, 3	jca 288	. 2 |- (F:A-->B -> (F Fn A /\ A.x e. A (F` x) e. B))
5		pm3.26 319	. . . 4 |- ((F Fn A /\ A.x e. A (F` x) e. B) -> F Fn A)
6		fvelrnb 3751	. . . . . . . 8 |- (F Fn A -> (y e. ran F <-> E.x e. A (F` x) = y))
7	6	biimpd 153	. . . . . . 7 |- (F Fn A -> (y e. ran F -> E.x e. A (F` x) = y))
8		hbra1 1684	. . . . . . . 8 |- (A.x e. A (F` x) e. B -> A.xA.x e. A (F` x) e. B)
9		ax-17 969	. . . . . . . 8 |- (y e. B -> A.x y e. B)
10		ra4 1691	. . . . . . . . 9 |- (A.x e. A (F` x) e. B -> (x e. A -> (F` x) e. B))
11		eleq1 1531	. . . . . . . . . 10 |- ((F` x) = y -> ((F` x) e. B <-> y e. B))
12	11	biimpcd 155	. . . . . . . . 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 1742	. . . . . . 7 |- (A.x e. A (F` x) e. B -> (E.x e. A (F` x) = y -> y e. B))
15	7, 14	sylan9 468	. . . . . 6 |- ((F Fn A /\ A.x e. A (F` x) e. B) -> (y e. ran F -> y e. B))
16	15	r19.21aiv 1710	. . . . 5 |- ((F Fn A /\ A.x e. A (F` x) e. B) -> A.y e. ran F y e. B)
17		dfss3 2055	. . . . 5 |- (ran F (_ B <-> A.y e. ran F y e. B)
18	16, 17	sylibr 200	. . . 4 |- ((F Fn A /\ A.x e. A (F` x) e. B) -> ran F (_ B)
19	5, 18	jca 288	. . 3 |- ((F Fn A /\ A.x e. A (F` x) e. B) -> (F Fn A /\ ran F (_ B))
20		df-f 3189	. . 3 |- (F:A-->B <-> (F Fn A /\ ran F (_ B))
21	19, 20	sylibr 200	. 2 |- ((F Fn A /\ A.x e. A (F` x) e. B) -> F:A-->B)
22	4, 21	impbi 157	1 |- (F:A-->B <-> (F Fn A /\ A.x e. A (F` x) e. B))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 954   e. wcel 956  A.wral 1642  E.wrex 1643   (_ wss 2043  ran crn 3166   Fn wfn 3172  -->wf 3173  ` cfv 3177

This theorem is referenced by:  ffnfvf 3820  fnfvrnss 3821  fopabfv 3822  abianfp 3953  ffnoprval 4005  elixpconst 4341  mapixp 4352  mapxpen 4481  unblem4 4526  alephfplem4 4879  ser1ref 6277  ser1f2 6279  shftf 6296  ser0f 6505  ref 6698  imf 6699  caure 6872  cauim 6873  ser1absdiflem 6874  serzref 6997  caucvg3a 7108  caucvg3lem 7110  cvgcmp2lem 7124  cvgcmp2clem 7126  cvgcmp3c 7130  eff 7263  eff2 7320  sinf 7390  cosf 7391  ubthlem6 8478  htthlem11 8573  efif 8655  pjmf1 9601

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-id 2830  df-xp 3179  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fun 3187  df-fn 3188  df-f 3189  df-fv 3193

Copyright terms: Public domain