Theorem elrnmpt 5917

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 5916	. 2 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
5	2, 4	elab2g 3637	1 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))

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

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 5245  ax-pr 5381

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-cnv 5642  df-dm 5644  df-rn 5645

This theorem is referenced by:  elrnmpt1s  5918  elrnmptd  5922  elrnmptdv  5924  elrnmpt2d  5925  nelrnmpt  5926  elimampt  6012  onnseq  8288  oarec  8501  fifo  9349  infpwfien  9986  fin23lem38  10273  fin1a2lem13  10336  ac6num  10403  isercoll2  15606  iserodd  16777  gsumwspan  18785  odf1o2  19519  mplcoe5lem  22011  neitr  23141  ordtbas2  23152  ordtopn1  23155  ordtopn2  23156  pnfnei  23181  mnfnei  23182  pnrmcld  23303  2ndcomap  23419  dis2ndc  23421  ptpjopn  23573  fbasrn  23845  elfm  23908  rnelfmlem  23913  rnelfm  23914  fmfnfmlem3  23917  fmfnfmlem4  23918  fmfnfm  23919  ptcmplem2  24014  tsmsfbas  24089  ustuqtoplem  24200  utopsnneiplem  24208  utopsnnei  24210  utopreg  24213  fmucnd  24252  neipcfilu  24256  imasdsf1olem  24334  xpsdsval  24342  met1stc  24482  metustel  24511  metustsym  24516  metuel2  24526  metustbl  24527  restmetu  24531  xrtgioo  24768  minveclem3b  25401  uniioombllem3  25559  dvivth  25988  gausslemma2dlem1a  27349  acunirnmpt  32755  acunirnmpt2  32756  acunirnmpt2f  32757  fnpreimac  32766  trsp2cyc  33223  elrgspnlem1  33342  elrgspnlem2  33343  elrgspn  33346  nsgqusf1olem2  33513  nsgqusf1olem3  33514  locfinreflem  34024  zarclsint  34056  zarcls  34058  ordtconnlem1  34108  esumcst  34247  esumrnmpt2  34252  measdivcstALTV  34409  oms0  34481  omssubadd  34484  cvmsss2  35496  poimirlem16  37916  poimirlem19  37919  poimirlem24  37924  poimirlem27  37927  itg2addnclem2  37952  suprnmpt  45562  rnmptpr  45565  wessf1ornlem  45573  disjrnmpt2  45576  disjf1o  45579  disjinfi  45580  choicefi  45587  rnmptlb  45630  rnmptbddlem  45631  rnmptbd2lem  45635  infnsuprnmpt  45637  elmptima  45645  supxrleubrnmpt  45793  suprleubrnmpt  45809  infrnmptle  45810  infxrunb3rnmpt  45815  supminfrnmpt  45832  infxrgelbrnmpt  45841  infrpgernmpt  45852  supminfxrrnmpt  45858  stoweidlem27  46414  stoweidlem31  46418  stoweidlem35  46422  stirlinglem5  46465  stirlinglem13  46473  fourierdlem80  46573  fourierdlem93  46586  fourierdlem103  46596  fourierdlem104  46597  subsaliuncllem  46744  subsaliuncl  46745  sge0rnn0  46755  sge00  46763  fsumlesge0  46764  sge0tsms  46767  sge0cl  46768  sge0f1o  46769  sge0fsum  46774  sge0supre  46776  sge0rnbnd  46780  sge0pnffigt  46783  sge0lefi  46785  sge0ltfirp  46787  sge0resplit  46793  sge0split  46796  sge0reuz  46834  sge0reuzb  46835  hoidmvlelem2  46983  smfpimcc  47195