Theorem elrnmpt 5922

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3053   ↦ cmpt 5188  ran crn 5639

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-mpt 5189  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  elrnmpt1s  5923  elrnmptd  5927  elrnmptdv  5929  elrnmpt2d  5930  elimampt  6014  onnseq  8313  oarec  8526  fifo  9383  infpwfien  10015  fin23lem38  10302  fin1a2lem13  10365  ac6num  10432  isercoll2  15635  iserodd  16806  gsumwspan  18773  odf1o2  19503  mplcoe5lem  21946  neitr  23067  ordtbas2  23078  ordtopn1  23081  ordtopn2  23082  pnfnei  23107  mnfnei  23108  pnrmcld  23229  2ndcomap  23345  dis2ndc  23347  ptpjopn  23499  fbasrn  23771  elfm  23834  rnelfmlem  23839  rnelfm  23840  fmfnfmlem3  23843  fmfnfmlem4  23844  fmfnfm  23845  ptcmplem2  23940  tsmsfbas  24015  ustuqtoplem  24127  utopsnneiplem  24135  utopsnnei  24137  utopreg  24140  fmucnd  24179  neipcfilu  24183  imasdsf1olem  24261  xpsdsval  24269  met1stc  24409  metustel  24438  metustsym  24443  metuel2  24453  metustbl  24454  restmetu  24458  xrtgioo  24695  minveclem3b  25328  uniioombllem3  25486  dvivth  25915  gausslemma2dlem1a  27276  acunirnmpt  32583  acunirnmpt2  32584  acunirnmpt2f  32585  fnpreimac  32595  trsp2cyc  33080  elrgspnlem1  33193  elrgspnlem2  33194  elrgspn  33197  nsgqusf1olem2  33385  nsgqusf1olem3  33386  locfinreflem  33830  zarclsint  33862  zarcls  33864  ordtconnlem1  33914  esumcst  34053  esumrnmpt2  34058  measdivcstALTV  34215  oms0  34288  omssubadd  34291  cvmsss2  35261  poimirlem16  37630  poimirlem19  37633  poimirlem24  37638  poimirlem27  37641  itg2addnclem2  37666  nelrnmpt  45078  suprnmpt  45168  rnmptpr  45171  wessf1ornlem  45179  disjrnmpt2  45182  disjf1o  45185  disjinfi  45186  choicefi  45194  rnmptlb  45237  rnmptbddlem  45238  rnmptbd2lem  45242  infnsuprnmpt  45244  elmptima  45252  supxrleubrnmpt  45402  suprleubrnmpt  45418  infrnmptle  45419  infxrunb3rnmpt  45424  supminfrnmpt  45441  infxrgelbrnmpt  45450  infrpgernmpt  45461  supminfxrrnmpt  45467  stoweidlem27  46025  stoweidlem31  46029  stoweidlem35  46033  stirlinglem5  46076  stirlinglem13  46084  fourierdlem80  46184  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  subsaliuncllem  46355  subsaliuncl  46356  sge0rnn0  46366  sge00  46374  fsumlesge0  46375  sge0tsms  46378  sge0cl  46379  sge0f1o  46380  sge0fsum  46385  sge0supre  46387  sge0rnbnd  46391  sge0pnffigt  46394  sge0lefi  46396  sge0ltfirp  46398  sge0resplit  46404  sge0split  46407  sge0reuz  46445  sge0reuzb  46446  hoidmvlelem2  46594  smfpimcc  46806