Theorem elrnmpt 5940

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∃wrex 3087   ↦ cmpt 5186  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  elrnmpt1s  5941  elrnmptd  5945  elrnmptdv  5947  elrnmpt2d  5948  nelrnmpt  5949  elimampt  6035  onnseq  8352  oarec  8570  fifo  9424  infpwfien  10141  fin23lem38  10427  fin1a2lem13  10490  ac6num  10557  isercoll2  15836  iserodd  17013  gsumwspan  19042  odf1o2  19787  mplcoe5lem  22348  neitr  23498  ordtbas2  23509  ordtopn1  23512  ordtopn2  23513  pnfnei  23538  mnfnei  23539  pnrmcld  23660  2ndcomap  23777  dis2ndc  23779  ptpjopn  23931  fbasrn  24203  elfm  24266  rnelfmlem  24271  rnelfm  24272  fmfnfmlem3  24275  fmfnfmlem4  24276  fmfnfm  24277  ptcmplem2  24372  tsmsfbas  24447  ustuqtoplem  24558  utopsnneiplem  24566  utopsnnei  24568  utopreg  24571  fmucnd  24610  neipcfilu  24614  imasdsf1olem  24692  xpsdsval  24700  met1stc  24840  metustel  24869  metustsym  24874  metuel2  24884  metustbl  24885  restmetu  24889  xrtgioo  25126  minveclem3b  25749  uniioombllem3  25906  dvivth  26330  gausslemma2dlem1a  27692  acunirnmpt  33253  acunirnmpt2  33254  acunirnmpt2f  33255  fnpreimac  33264  trsp2cyc  33684  elrgspnlem1  33803  elrgspnlem2  33804  elrgspn  33807  nsgqusf1olem2  33965  nsgqusf1olem3  33966  locfinreflem  34472  zarclsint  34504  zarcls  34506  ordtconnlem1  34556  esumcst  34695  esumrnmpt2  34700  measdivcstALTV  34858  oms0  34929  omssubadd  34932  cvmsss2  36039  poimirlem16  38554  poimirlem19  38557  poimirlem24  38562  poimirlem27  38565  itg2addnclem2  38590  suprnmpt  46188  rnmptpr  46191  wessf1ornlem  46199  disjrnmpt2  46202  disjf1o  46205  disjinfi  46206  choicefi  46213  rnmptlb  46254  rnmptbddlem  46255  rnmptbd2lem  46259  infnsuprnmpt  46261  elmptima  46269  supxrleubrnmpt  46415  suprleubrnmpt  46431  infrnmptle  46432  infxrunb3rnmpt  46437  supminfrnmpt  46454  infxrgelbrnmpt  46463  infrpgernmpt  46474  supminfxrrnmpt  46480  stoweidlem27  47036  stoweidlem31  47040  stoweidlem35  47044  stirlinglem5  47087  stirlinglem13  47095  fourierdlem80  47195  fourierdlem93  47208  fourierdlem103  47218  fourierdlem104  47219  subsaliuncllem  47366  subsaliuncl  47367  sge0rnn0  47377  sge00  47385  fsumlesge0  47386  sge0tsms  47389  sge0cl  47390  sge0f1o  47391  sge0fsum  47396  sge0supre  47398  sge0rnbnd  47402  sge0pnffigt  47405  sge0lefi  47407  sge0ltfirp  47409  sge0resplit  47415  sge0split  47418  sge0reuz  47456  sge0reuzb  47457  hoidmvlelem2  47605  smfpimcc  47817