Theorem elrnmpt 5913

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3061   ↦ cmpt 5166  ran crn 5632

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-mpt 5167  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  elrnmpt1s  5914  elrnmptd  5918  elrnmptdv  5920  elrnmpt2d  5921  nelrnmpt  5922  elimampt  6008  onnseq  8284  oarec  8497  fifo  9345  infpwfien  9984  fin23lem38  10271  fin1a2lem13  10334  ac6num  10401  isercoll2  15631  iserodd  16806  gsumwspan  18814  odf1o2  19548  mplcoe5lem  22017  neitr  23145  ordtbas2  23156  ordtopn1  23159  ordtopn2  23160  pnfnei  23185  mnfnei  23186  pnrmcld  23307  2ndcomap  23423  dis2ndc  23425  ptpjopn  23577  fbasrn  23849  elfm  23912  rnelfmlem  23917  rnelfm  23918  fmfnfmlem3  23921  fmfnfmlem4  23922  fmfnfm  23923  ptcmplem2  24018  tsmsfbas  24093  ustuqtoplem  24204  utopsnneiplem  24212  utopsnnei  24214  utopreg  24217  fmucnd  24256  neipcfilu  24260  imasdsf1olem  24338  xpsdsval  24346  met1stc  24486  metustel  24515  metustsym  24520  metuel2  24530  metustbl  24531  restmetu  24535  xrtgioo  24772  minveclem3b  25395  uniioombllem3  25552  dvivth  25977  gausslemma2dlem1a  27328  acunirnmpt  32732  acunirnmpt2  32733  acunirnmpt2f  32734  fnpreimac  32743  trsp2cyc  33184  elrgspnlem1  33303  elrgspnlem2  33304  elrgspn  33307  nsgqusf1olem2  33474  nsgqusf1olem3  33475  locfinreflem  33984  zarclsint  34016  zarcls  34018  ordtconnlem1  34068  esumcst  34207  esumrnmpt2  34212  measdivcstALTV  34369  oms0  34441  omssubadd  34444  cvmsss2  35456  poimirlem16  37957  poimirlem19  37960  poimirlem24  37965  poimirlem27  37968  itg2addnclem2  37993  suprnmpt  45604  rnmptpr  45607  wessf1ornlem  45615  disjrnmpt2  45618  disjf1o  45621  disjinfi  45622  choicefi  45629  rnmptlb  45672  rnmptbddlem  45673  rnmptbd2lem  45677  infnsuprnmpt  45679  elmptima  45687  supxrleubrnmpt  45834  suprleubrnmpt  45850  infrnmptle  45851  infxrunb3rnmpt  45856  supminfrnmpt  45873  infxrgelbrnmpt  45882  infrpgernmpt  45893  supminfxrrnmpt  45899  stoweidlem27  46455  stoweidlem31  46459  stoweidlem35  46463  stirlinglem5  46506  stirlinglem13  46514  fourierdlem80  46614  fourierdlem93  46627  fourierdlem103  46637  fourierdlem104  46638  subsaliuncllem  46785  subsaliuncl  46786  sge0rnn0  46796  sge00  46804  fsumlesge0  46805  sge0tsms  46808  sge0cl  46809  sge0f1o  46810  sge0fsum  46815  sge0supre  46817  sge0rnbnd  46821  sge0pnffigt  46824  sge0lefi  46826  sge0ltfirp  46828  sge0resplit  46834  sge0split  46837  sge0reuz  46875  sge0reuzb  46876  hoidmvlelem2  47024  smfpimcc  47236