Theorem elrnmpt 5953

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∃wrex 3070   ↦ cmpt 5230  ran crn 5676

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-mpt 5231  df-cnv 5683  df-dm 5685  df-rn 5686

This theorem is referenced by:  elrnmpt1s  5954  elrnmptd  5958  elrnmptdv  5959  elrnmpt2d  5960  onnseq  8340  oarec  8558  fifo  9423  infpwfien  10053  fin23lem38  10340  fin1a2lem13  10403  ac6num  10470  isercoll2  15611  iserodd  16764  gsumwspan  18723  odf1o2  19435  mplcoe5lem  21585  neitr  22675  ordtbas2  22686  ordtopn1  22689  ordtopn2  22690  pnfnei  22715  mnfnei  22716  pnrmcld  22837  2ndcomap  22953  dis2ndc  22955  ptpjopn  23107  fbasrn  23379  elfm  23442  rnelfmlem  23447  rnelfm  23448  fmfnfmlem3  23451  fmfnfmlem4  23452  fmfnfm  23453  ptcmplem2  23548  tsmsfbas  23623  ustuqtoplem  23735  utopsnneiplem  23743  utopsnnei  23745  utopreg  23748  fmucnd  23788  neipcfilu  23792  imasdsf1olem  23870  xpsdsval  23878  met1stc  24021  metustel  24050  metustsym  24055  metuel2  24065  metustbl  24066  restmetu  24070  xrtgioo  24313  minveclem3b  24936  uniioombllem3  25093  dvivth  25518  gausslemma2dlem1a  26857  elimampt  31849  acunirnmpt  31871  acunirnmpt2  31872  acunirnmpt2f  31873  fnpreimac  31883  trsp2cyc  32269  nsgqusf1olem2  32513  nsgqusf1olem3  32514  locfinreflem  32808  zarclsint  32840  zarcls  32842  ordtconnlem1  32892  esumcst  33049  esumrnmpt2  33054  measdivcstALTV  33211  oms0  33284  omssubadd  33287  cvmsss2  34253  poimirlem16  36492  poimirlem19  36495  poimirlem24  36500  poimirlem27  36503  itg2addnclem2  36528  nelrnmpt  43758  suprnmpt  43855  rnmptpr  43858  wessf1ornlem  43867  disjrnmpt2  43871  disjf1o  43874  disjinfi  43876  choicefi  43884  rnmptlb  43932  rnmptbddlem  43933  rnmptbd2lem  43938  infnsuprnmpt  43940  elmptima  43948  supxrleubrnmpt  44102  suprleubrnmpt  44118  infrnmptle  44119  infxrunb3rnmpt  44124  supminfrnmpt  44141  infxrgelbrnmpt  44150  infrpgernmpt  44161  supminfxrrnmpt  44167  stoweidlem27  44729  stoweidlem31  44733  stoweidlem35  44737  stirlinglem5  44780  stirlinglem13  44788  fourierdlem80  44888  fourierdlem93  44901  fourierdlem103  44911  fourierdlem104  44912  subsaliuncllem  45059  subsaliuncl  45060  sge0rnn0  45070  sge00  45078  fsumlesge0  45079  sge0tsms  45082  sge0cl  45083  sge0f1o  45084  sge0fsum  45089  sge0supre  45091  sge0rnbnd  45095  sge0pnffigt  45098  sge0lefi  45100  sge0ltfirp  45102  sge0resplit  45108  sge0split  45111  sge0reuz  45149  sge0reuzb  45150  hoidmvlelem2  45298  smfpimcc  45510