Theorem fvelrnb 3766

Description: A member of a function's range is a value of the function.

Assertion

Ref	Expression
fvelrnb	|- (F Fn A -> (B e. ran F <-> E.x e. A (F` x) = B))

Distinct variable groups:   x,A   x,B   x,F

Proof of Theorem fvelrnb

Step	Hyp	Ref	Expression
1		fnrnfv 3765	. . 3 |- (F Fn A -> ran F = {y | E.x e. A y = (F` x)})
2	1	eleq2d 1544	. 2 |- (F Fn A -> (B e. ran F <-> B e. {y | E.x e. A y = (F` x)}))
3		fvex 3738	. . . . . 6 |- (F` x) e. V
4		eleq1 1537	. . . . . 6 |- ((F` x) = B -> ((F` x) e. V <-> B e. V))
5	3, 4	mpbii 193	. . . . 5 |- ((F` x) = B -> B e. V)
6	5	a1i 8	. . . 4 |- (x e. A -> ((F` x) = B -> B e. V))
7	6	r19.23aiv 1746	. . 3 |- (E.x e. A (F` x) = B -> B e. V)
8		eqeq1 1484	. . . . 5 |- (y = B -> (y = (F` x) <-> B = (F` x)))
9		eqcom 1480	. . . . 5 |- (B = (F` x) <-> (F` x) = B)
10	8, 9	syl6bb 538	. . . 4 |- (y = B -> (y = (F` x) <-> (F` x) = B))
11	10	rexbidv 1667	. . 3 |- (y = B -> (E.x e. A y = (F` x) <-> E.x e. A (F` x) = B))
12	7, 11	elab3 1906	. 2 |- (B e. {y | E.x e. A y = (F` x)} <-> E.x e. A (F` x) = B)
13	2, 12	syl6bb 538	1 |- (F Fn A -> (B e. ran F <-> E.x e. A (F` x) = B))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 958   e. wcel 960  {cab 1466  E.wrex 1649  Vcvv 1814  ran crn 3177   Fn wfn 3183  ` cfv 3188

This theorem is referenced by:  elrnopabg 3806  chfnrn 3808  ffnfv 3834  fconstfv 3855  elunirnALT 3875  isoini 3906  canth 3913  elrnoprabg 4130  mapenlem2 4496  inf0 4615  inf3lem6 4627  noinfep 4650  aceq5 4750  zorn2lem4 4801  isinfcard 4898  om2uzran 6301  fsequb2 6525  seq1ublem 6911  climsup 7155  cvgcmpub 7185  reeff1o 7426  unbenlem 7505  ruclem33 7543  ruclem35 7545  ruclem37 7547  ghgrpilem2 8130  ubthlem6 8530  bra11 10036  cnvbravalt 10038  pjssdif1 10098  pjhmopidm 10105  ghomgrpilem2 10381

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748  ax-pr 2785  ax-un 2872

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-rex 1653  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-id 2841  df-xp 3190  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-fv 3204

Copyright terms: Public domain