Theorem elrnmpt 5942

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

Hypothesis

Ref	Expression
rnmpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
elrnmpt	⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))

Distinct variable group:   𝑥,𝐶

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem elrnmpt

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2764	. . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐵 ↔ 𝐶 = 𝐵))
2	1	rexbidv 3186	. 2 ⊢ (𝑦 = 𝐶 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
3		rnmpt.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	rnmpt 5941	. 2 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
5	2, 4	elab2g 3634	1 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∃wrex 3086   ↦ cmpt 5186  ran crn 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  elrnmpt1s  5943  elrnmptd  5947  elrnmptdv  5949  elrnmpt2d  5950  nelrnmpt  5951  elimampt  6039  onnseq  8334  oarec  8552  fifo  9405  infpwfien  10068  fin23lem38  10354  fin1a2lem13  10417  ac6num  10484  isercoll2  15759  iserodd  16930  gsumwspan  18958  odf1o2  19703  mplcoe5lem  22258  neitr  23408  ordtbas2  23419  ordtopn1  23422  ordtopn2  23423  pnfnei  23448  mnfnei  23449  pnrmcld  23570  2ndcomap  23687  dis2ndc  23689  ptpjopn  23841  fbasrn  24113  elfm  24176  rnelfmlem  24181  rnelfm  24182  fmfnfmlem3  24185  fmfnfmlem4  24186  fmfnfm  24187  ptcmplem2  24282  tsmsfbas  24357  ustuqtoplem  24468  utopsnneiplem  24476  utopsnnei  24478  utopreg  24481  fmucnd  24520  neipcfilu  24524  imasdsf1olem  24602  xpsdsval  24610  met1stc  24750  metustel  24779  metustsym  24784  metuel2  24794  metustbl  24795  restmetu  24799  xrtgioo  25036  minveclem3b  25659  uniioombllem3  25816  dvivth  26240  gausslemma2dlem1a  27604  acunirnmpt  33135  acunirnmpt2  33136  acunirnmpt2f  33137  fnpreimac  33146  trsp2cyc  33566  elrgspnlem1  33685  elrgspnlem2  33686  elrgspn  33689  nsgqusf1olem2  33846  nsgqusf1olem3  33847  locfinreflem  34353  zarclsint  34385  zarcls  34387  ordtconnlem1  34437  esumcst  34576  esumrnmpt2  34581  measdivcstALTV  34739  oms0  34811  omssubadd  34814  cvmsss2  35856  poimirlem16  38388  poimirlem19  38391  poimirlem24  38396  poimirlem27  38399  itg2addnclem2  38424  suprnmpt  46009  rnmptpr  46012  wessf1ornlem  46020  disjrnmpt2  46023  disjf1o  46026  disjinfi  46027  choicefi  46034  rnmptlb  46075  rnmptbddlem  46076  rnmptbd2lem  46080  infnsuprnmpt  46082  elmptima  46090  supxrleubrnmpt  46237  suprleubrnmpt  46253  infrnmptle  46254  infxrunb3rnmpt  46259  supminfrnmpt  46276  infxrgelbrnmpt  46285  infrpgernmpt  46296  supminfxrrnmpt  46302  stoweidlem27  46858  stoweidlem31  46862  stoweidlem35  46866  stirlinglem5  46909  stirlinglem13  46917  fourierdlem80  47017  fourierdlem93  47030  fourierdlem103  47040  fourierdlem104  47041  subsaliuncllem  47188  subsaliuncl  47189  sge0rnn0  47199  sge00  47207  fsumlesge0  47208  sge0tsms  47211  sge0cl  47212  sge0f1o  47213  sge0fsum  47218  sge0supre  47220  sge0rnbnd  47224  sge0pnffigt  47227  sge0lefi  47229  sge0ltfirp  47231  sge0resplit  47237  sge0split  47240  sge0reuz  47278  sge0reuzb  47279  hoidmvlelem2  47427  smfpimcc  47639