Theorem elrnmpt 5092

Description: The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015.)

Hypothesis

Ref	Expression
rnmpt.1	|- F = ( x e. A |-> B )

Assertion

Ref	Expression
elrnmpt	|- ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )

Distinct variable group:   x, C

Allowed substitution hints:   A( x)   B( x)   F( x)   V( x)

Proof of Theorem elrnmpt

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2424	. . 3 |- ( y = C -> ( y = B <-> C = B ) )
2	1	rexbidv 2937	. 2 |- ( y = C -> ( E. x e. A y = B <-> E. x e. A C = B ) )
3		rnmpt.1	. . 3 |- F = ( x e. A |-> B )
4	3	rnmpt 5091	. 2 |- ran F = { y | E. x e. A y = B }
5	2, 4	elab2g 3217	1 |- ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )

Syntax hints:   -> wi 4   <-> wb 187   = wceq 1437   e. wcel 1867   E.wrex 2774   |-> cmpt 4475   ran crn 4846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418  df-opab 4476  df-mpt 4477  df-cnv 4853  df-dm 4855  df-rn 4856

This theorem is referenced by:  elrnmpt1s  5093  onnseq  7062  oarec  7262  fifo  7943  infpwfien  8482  fin23lem38  8768  fin1a2lem13  8831  ac6num  8898  isercoll2  13699  iserodd  14737  gsumwspan  16574  odf1o2  17153  mplcoe5lem  18619  neitr  20120  ordtbas2  20131  ordtopn1  20134  ordtopn2  20135  pnfnei  20160  mnfnei  20161  pnrmcld  20282  2ndcomap  20397  dis2ndc  20399  ptpjopn  20551  fbasrn  20823  elfm  20886  rnelfmlem  20891  rnelfm  20892  fmfnfmlem3  20895  fmfnfmlem4  20896  fmfnfm  20897  ptcmplem2  20992  tsmsfbas  21066  ustuqtoplem  21178  utopsnneiplem  21186  utopsnnei  21188  utopreg  21191  fmucnd  21231  neipcfilu  21235  imasdsf1olem  21312  xpsdsval  21320  met1stc  21460  metustel  21489  metustsym  21494  metuel2  21504  metustbl  21505  restmetu  21509  xrtgioo  21748  minveclem3b  22276  uniioombllem3  22437  dvivth  22856  acunirnmpt  28127  acunirnmpt2  28128  acunirnmpt2f  28129  locfinreflem  28532  ordtconlem1  28595  esumcst  28749  esumrnmpt2  28754  measdivcstOLD  28911  oms0  28984  omssubadd  28987  cvmsss2  29811  poimirlem16  31689  poimirlem19  31692  poimirlem24  31697  poimirlem27  31700  itg2addnclem2  31727  suprnmpt  37094  rnmptpr  37099  elrnmptd  37109  rnmptssrn  37112  wessf1ornlem  37115  disjrnmpt2  37119  disjf1o  37122  disjinfi  37124  stoweidlem27  37489  stoweidlem31  37494  stoweidlem35  37498  stirlinglem5  37542  stirlinglem13  37550  fourierdlem53  37624  fourierdlem80  37651  fourierdlem93  37664  fourierdlem103  37674  fourierdlem104  37675  sge0rnn0  37777  sge00  37785  fsumlesge0  37786  sge0tsms  37789  sge0cl  37790  sge0f1o  37791  sge0fsum  37796  sge0supre  37798  sge0rnbnd  37802  sge0pnffigt  37805  sge0lefi  37807  sge0ltfirp  37809  sge0resplit  37815  sge0split  37818