Theorem elrnmpt 5854

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  ∃wrex 3064   ↦ cmpt 5153  ran crn 5581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-mpt 5154  df-cnv 5588  df-dm 5590  df-rn 5591

This theorem is referenced by:  elrnmpt1s  5855  elrnmptd  5859  elrnmptdv  5860  elrnmpt2d  5861  onnseq  8146  oarec  8355  fifo  9121  infpwfien  9749  fin23lem38  10036  fin1a2lem13  10099  ac6num  10166  isercoll2  15308  iserodd  16464  gsumwspan  18400  odf1o2  19093  mplcoe5lem  21150  neitr  22239  ordtbas2  22250  ordtopn1  22253  ordtopn2  22254  pnfnei  22279  mnfnei  22280  pnrmcld  22401  2ndcomap  22517  dis2ndc  22519  ptpjopn  22671  fbasrn  22943  elfm  23006  rnelfmlem  23011  rnelfm  23012  fmfnfmlem3  23015  fmfnfmlem4  23016  fmfnfm  23017  ptcmplem2  23112  tsmsfbas  23187  ustuqtoplem  23299  utopsnneiplem  23307  utopsnnei  23309  utopreg  23312  fmucnd  23352  neipcfilu  23356  imasdsf1olem  23434  xpsdsval  23442  met1stc  23583  metustel  23612  metustsym  23617  metuel2  23627  metustbl  23628  restmetu  23632  xrtgioo  23875  minveclem3b  24497  uniioombllem3  24654  dvivth  25079  gausslemma2dlem1a  26418  elimampt  30874  acunirnmpt  30898  acunirnmpt2  30899  acunirnmpt2f  30900  fnpreimac  30910  trsp2cyc  31292  nsgqusf1olem2  31501  nsgqusf1olem3  31502  locfinreflem  31692  zarclsint  31724  zarcls  31726  ordtconnlem1  31776  esumcst  31931  esumrnmpt2  31936  measdivcstALTV  32093  oms0  32164  omssubadd  32167  cvmsss2  33136  poimirlem16  35720  poimirlem19  35723  poimirlem24  35728  poimirlem27  35731  itg2addnclem2  35756  nelrnmpt  42523  suprnmpt  42599  rnmptpr  42602  wessf1ornlem  42611  disjrnmpt2  42615  disjf1o  42618  disjinfi  42620  choicefi  42629  rnmptlb  42677  rnmptbddlem  42678  rnmptbd2lem  42683  infnsuprnmpt  42685  elmptima  42693  supxrleubrnmpt  42836  suprleubrnmpt  42852  infrnmptle  42853  infxrunb3rnmpt  42858  supminfrnmpt  42875  infxrgelbrnmpt  42884  infrpgernmpt  42895  supminfxrrnmpt  42901  stoweidlem27  43458  stoweidlem31  43462  stoweidlem35  43466  stirlinglem5  43509  stirlinglem13  43517  fourierdlem80  43617  fourierdlem93  43630  fourierdlem103  43640  fourierdlem104  43641  subsaliuncllem  43786  subsaliuncl  43787  sge0rnn0  43796  sge00  43804  fsumlesge0  43805  sge0tsms  43808  sge0cl  43809  sge0f1o  43810  sge0fsum  43815  sge0supre  43817  sge0rnbnd  43821  sge0pnffigt  43824  sge0lefi  43826  sge0ltfirp  43828  sge0resplit  43834  sge0split  43837  sge0reuz  43875  sge0reuzb  43876  hoidmvlelem2  44024  smfpimcc  44228