Theorem elrnmpt 5936

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562   ∈ wcel 2144  ∃wrex 3088   ↦ cmpt 5183  ran crn 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-opab 5165  df-mpt 5184  df-cnv 5657  df-dm 5659  df-rn 5660

This theorem is referenced by:  elrnmpt1s  5937  elrnmptd  5941  elrnmptdv  5943  elrnmpt2d  5944  nelrnmpt  5945  elimampt  6034  onnseq  8317  oarec  8533  fifo  9380  infpwfien  10020  fin23lem38  10308  fin1a2lem13  10371  ac6num  10438  isercoll2  15698  iserodd  16873  gsumwspan  18882  odf1o2  19615  mplcoe5lem  22094  neitr  23242  ordtbas2  23253  ordtopn1  23256  ordtopn2  23257  pnfnei  23282  mnfnei  23283  pnrmcld  23404  2ndcomap  23520  dis2ndc  23522  ptpjopn  23674  fbasrn  23946  elfm  24009  rnelfmlem  24014  rnelfm  24015  fmfnfmlem3  24018  fmfnfmlem4  24019  fmfnfm  24020  ptcmplem2  24115  tsmsfbas  24190  ustuqtoplem  24301  utopsnneiplem  24309  utopsnnei  24311  utopreg  24314  fmucnd  24353  neipcfilu  24357  imasdsf1olem  24435  xpsdsval  24443  met1stc  24583  metustel  24612  metustsym  24617  metuel2  24627  metustbl  24628  restmetu  24632  xrtgioo  24869  minveclem3b  25492  uniioombllem3  25649  dvivth  26074  gausslemma2dlem1a  27431  acunirnmpt  32863  acunirnmpt2  32864  acunirnmpt2f  32865  fnpreimac  32874  trsp2cyc  33305  elrgspnlem1  33425  elrgspnlem2  33426  elrgspn  33429  nsgqusf1olem2  33602  nsgqusf1olem3  33603  locfinreflem  34139  zarclsint  34171  zarcls  34173  ordtconnlem1  34223  esumcst  34362  esumrnmpt2  34367  measdivcstALTV  34524  oms0  34596  omssubadd  34599  cvmsss2  35629  poimirlem16  38140  poimirlem19  38143  poimirlem24  38148  poimirlem27  38151  itg2addnclem2  38176  suprnmpt  45757  rnmptpr  45760  wessf1ornlem  45768  disjrnmpt2  45771  disjf1o  45774  disjinfi  45775  choicefi  45782  rnmptlb  45823  rnmptbddlem  45824  rnmptbd2lem  45828  infnsuprnmpt  45830  elmptima  45838  supxrleubrnmpt  45985  suprleubrnmpt  46001  infrnmptle  46002  infxrunb3rnmpt  46007  supminfrnmpt  46024  infxrgelbrnmpt  46033  infrpgernmpt  46044  supminfxrrnmpt  46050  stoweidlem27  46606  stoweidlem31  46610  stoweidlem35  46614  stirlinglem5  46657  stirlinglem13  46665  fourierdlem80  46765  fourierdlem93  46778  fourierdlem103  46788  fourierdlem104  46789  subsaliuncllem  46936  subsaliuncl  46937  sge0rnn0  46947  sge00  46955  fsumlesge0  46956  sge0tsms  46959  sge0cl  46960  sge0f1o  46961  sge0fsum  46966  sge0supre  46968  sge0rnbnd  46972  sge0pnffigt  46975  sge0lefi  46977  sge0ltfirp  46979  sge0resplit  46985  sge0split  46988  sge0reuz  47026  sge0reuzb  47027  hoidmvlelem2  47175  smfpimcc  47387