Theorem elrnmpt 5864

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2110  ∃wrex 3067   ↦ cmpt 5162  ran crn 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-mpt 5163  df-cnv 5598  df-dm 5600  df-rn 5601

This theorem is referenced by:  elrnmpt1s  5865  elrnmptd  5869  elrnmptdv  5870  elrnmpt2d  5871  onnseq  8166  oarec  8378  fifo  9169  infpwfien  9819  fin23lem38  10106  fin1a2lem13  10169  ac6num  10236  isercoll2  15378  iserodd  16534  gsumwspan  18483  odf1o2  19176  mplcoe5lem  21238  neitr  22329  ordtbas2  22340  ordtopn1  22343  ordtopn2  22344  pnfnei  22369  mnfnei  22370  pnrmcld  22491  2ndcomap  22607  dis2ndc  22609  ptpjopn  22761  fbasrn  23033  elfm  23096  rnelfmlem  23101  rnelfm  23102  fmfnfmlem3  23105  fmfnfmlem4  23106  fmfnfm  23107  ptcmplem2  23202  tsmsfbas  23277  ustuqtoplem  23389  utopsnneiplem  23397  utopsnnei  23399  utopreg  23402  fmucnd  23442  neipcfilu  23446  imasdsf1olem  23524  xpsdsval  23532  met1stc  23675  metustel  23704  metustsym  23709  metuel2  23719  metustbl  23720  restmetu  23724  xrtgioo  23967  minveclem3b  24590  uniioombllem3  24747  dvivth  25172  gausslemma2dlem1a  26511  elimampt  30969  acunirnmpt  30992  acunirnmpt2  30993  acunirnmpt2f  30994  fnpreimac  31004  trsp2cyc  31386  nsgqusf1olem2  31595  nsgqusf1olem3  31596  locfinreflem  31786  zarclsint  31818  zarcls  31820  ordtconnlem1  31870  esumcst  32027  esumrnmpt2  32032  measdivcstALTV  32189  oms0  32260  omssubadd  32263  cvmsss2  33232  poimirlem16  35789  poimirlem19  35792  poimirlem24  35797  poimirlem27  35800  itg2addnclem2  35825  nelrnmpt  42604  suprnmpt  42680  rnmptpr  42683  wessf1ornlem  42692  disjrnmpt2  42696  disjf1o  42699  disjinfi  42701  choicefi  42710  rnmptlb  42758  rnmptbddlem  42759  rnmptbd2lem  42764  infnsuprnmpt  42766  elmptima  42774  supxrleubrnmpt  42917  suprleubrnmpt  42933  infrnmptle  42934  infxrunb3rnmpt  42939  supminfrnmpt  42956  infxrgelbrnmpt  42965  infrpgernmpt  42976  supminfxrrnmpt  42982  stoweidlem27  43539  stoweidlem31  43543  stoweidlem35  43547  stirlinglem5  43590  stirlinglem13  43598  fourierdlem80  43698  fourierdlem93  43711  fourierdlem103  43721  fourierdlem104  43722  subsaliuncllem  43867  subsaliuncl  43868  sge0rnn0  43877  sge00  43885  fsumlesge0  43886  sge0tsms  43889  sge0cl  43890  sge0f1o  43891  sge0fsum  43896  sge0supre  43898  sge0rnbnd  43902  sge0pnffigt  43905  sge0lefi  43907  sge0ltfirp  43909  sge0resplit  43915  sge0split  43918  sge0reuz  43956  sge0reuzb  43957  hoidmvlelem2  44105  smfpimcc  44309