Theorem elrnmpt 5909

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 2741	. . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐵 ↔ 𝐶 = 𝐵))
2	1	rexbidv 3162	. 2 ⊢ (𝑦 = 𝐶 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
3		rnmpt.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	rnmpt 5908	. 2 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
5	2, 4	elab2g 3624	1 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3062   ↦ cmpt 5167  ran crn 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-cnv 5634  df-dm 5636  df-rn 5637

This theorem is referenced by:  elrnmpt1s  5910  elrnmptd  5914  elrnmptdv  5916  elrnmpt2d  5917  nelrnmpt  5918  elimampt  6004  onnseq  8279  oarec  8492  fifo  9340  infpwfien  9979  fin23lem38  10266  fin1a2lem13  10329  ac6num  10396  isercoll2  15626  iserodd  16801  gsumwspan  18809  odf1o2  19543  mplcoe5lem  22031  neitr  23159  ordtbas2  23170  ordtopn1  23173  ordtopn2  23174  pnfnei  23199  mnfnei  23200  pnrmcld  23321  2ndcomap  23437  dis2ndc  23439  ptpjopn  23591  fbasrn  23863  elfm  23926  rnelfmlem  23931  rnelfm  23932  fmfnfmlem3  23935  fmfnfmlem4  23936  fmfnfm  23937  ptcmplem2  24032  tsmsfbas  24107  ustuqtoplem  24218  utopsnneiplem  24226  utopsnnei  24228  utopreg  24231  fmucnd  24270  neipcfilu  24274  imasdsf1olem  24352  xpsdsval  24360  met1stc  24500  metustel  24529  metustsym  24534  metuel2  24544  metustbl  24545  restmetu  24549  xrtgioo  24786  minveclem3b  25409  uniioombllem3  25566  dvivth  25991  gausslemma2dlem1a  27346  acunirnmpt  32751  acunirnmpt2  32752  acunirnmpt2f  32753  fnpreimac  32762  trsp2cyc  33203  elrgspnlem1  33322  elrgspnlem2  33323  elrgspn  33326  nsgqusf1olem2  33493  nsgqusf1olem3  33494  locfinreflem  34004  zarclsint  34036  zarcls  34038  ordtconnlem1  34088  esumcst  34227  esumrnmpt2  34232  measdivcstALTV  34389  oms0  34461  omssubadd  34464  cvmsss2  35476  poimirlem16  37975  poimirlem19  37978  poimirlem24  37983  poimirlem27  37986  itg2addnclem2  38011  suprnmpt  45626  rnmptpr  45629  wessf1ornlem  45637  disjrnmpt2  45640  disjf1o  45643  disjinfi  45644  choicefi  45651  rnmptlb  45694  rnmptbddlem  45695  rnmptbd2lem  45699  infnsuprnmpt  45701  elmptima  45709  supxrleubrnmpt  45856  suprleubrnmpt  45872  infrnmptle  45873  infxrunb3rnmpt  45878  supminfrnmpt  45895  infxrgelbrnmpt  45904  infrpgernmpt  45915  supminfxrrnmpt  45921  stoweidlem27  46477  stoweidlem31  46481  stoweidlem35  46485  stirlinglem5  46528  stirlinglem13  46536  fourierdlem80  46636  fourierdlem93  46649  fourierdlem103  46659  fourierdlem104  46660  subsaliuncllem  46807  subsaliuncl  46808  sge0rnn0  46818  sge00  46826  fsumlesge0  46827  sge0tsms  46830  sge0cl  46831  sge0f1o  46832  sge0fsum  46837  sge0supre  46839  sge0rnbnd  46843  sge0pnffigt  46846  sge0lefi  46848  sge0ltfirp  46850  sge0resplit  46856  sge0split  46859  sge0reuz  46897  sge0reuzb  46898  hoidmvlelem2  47046  smfpimcc  47258