Theorem elrnmpt 5943

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3061   ↦ cmpt 5206  ran crn 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-mpt 5207  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  elrnmpt1s  5944  elrnmptd  5948  elrnmptdv  5950  elrnmpt2d  5951  elimampt  6035  onnseq  8363  oarec  8579  fifo  9449  infpwfien  10081  fin23lem38  10368  fin1a2lem13  10431  ac6num  10498  isercoll2  15690  iserodd  16860  gsumwspan  18829  odf1o2  19559  mplcoe5lem  22002  neitr  23123  ordtbas2  23134  ordtopn1  23137  ordtopn2  23138  pnfnei  23163  mnfnei  23164  pnrmcld  23285  2ndcomap  23401  dis2ndc  23403  ptpjopn  23555  fbasrn  23827  elfm  23890  rnelfmlem  23895  rnelfm  23896  fmfnfmlem3  23899  fmfnfmlem4  23900  fmfnfm  23901  ptcmplem2  23996  tsmsfbas  24071  ustuqtoplem  24183  utopsnneiplem  24191  utopsnnei  24193  utopreg  24196  fmucnd  24235  neipcfilu  24239  imasdsf1olem  24317  xpsdsval  24325  met1stc  24465  metustel  24494  metustsym  24499  metuel2  24509  metustbl  24510  restmetu  24514  xrtgioo  24751  minveclem3b  25385  uniioombllem3  25543  dvivth  25972  gausslemma2dlem1a  27333  acunirnmpt  32642  acunirnmpt2  32643  acunirnmpt2f  32644  fnpreimac  32654  trsp2cyc  33139  elrgspnlem1  33242  elrgspnlem2  33243  elrgspn  33246  nsgqusf1olem2  33434  nsgqusf1olem3  33435  locfinreflem  33876  zarclsint  33908  zarcls  33910  ordtconnlem1  33960  esumcst  34099  esumrnmpt2  34104  measdivcstALTV  34261  oms0  34334  omssubadd  34337  cvmsss2  35301  poimirlem16  37665  poimirlem19  37668  poimirlem24  37673  poimirlem27  37676  itg2addnclem2  37701  nelrnmpt  45088  suprnmpt  45178  rnmptpr  45181  wessf1ornlem  45189  disjrnmpt2  45192  disjf1o  45195  disjinfi  45196  choicefi  45204  rnmptlb  45247  rnmptbddlem  45248  rnmptbd2lem  45252  infnsuprnmpt  45254  elmptima  45262  supxrleubrnmpt  45413  suprleubrnmpt  45429  infrnmptle  45430  infxrunb3rnmpt  45435  supminfrnmpt  45452  infxrgelbrnmpt  45461  infrpgernmpt  45472  supminfxrrnmpt  45478  stoweidlem27  46036  stoweidlem31  46040  stoweidlem35  46044  stirlinglem5  46087  stirlinglem13  46095  fourierdlem80  46195  fourierdlem93  46208  fourierdlem103  46218  fourierdlem104  46219  subsaliuncllem  46366  subsaliuncl  46367  sge0rnn0  46377  sge00  46385  fsumlesge0  46386  sge0tsms  46389  sge0cl  46390  sge0f1o  46391  sge0fsum  46396  sge0supre  46398  sge0rnbnd  46402  sge0pnffigt  46405  sge0lefi  46407  sge0ltfirp  46409  sge0resplit  46415  sge0split  46418  sge0reuz  46456  sge0reuzb  46457  hoidmvlelem2  46605  smfpimcc  46817