Theorem elrnmpt 5905

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∃wrex 3058   ↦ cmpt 5177  ran crn 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-mpt 5178  df-cnv 5630  df-dm 5632  df-rn 5633

This theorem is referenced by:  elrnmpt1s  5906  elrnmptd  5910  elrnmptdv  5912  elrnmpt2d  5913  nelrnmpt  5914  elimampt  6000  onnseq  8274  oarec  8487  fifo  9333  infpwfien  9970  fin23lem38  10257  fin1a2lem13  10320  ac6num  10387  isercoll2  15590  iserodd  16761  gsumwspan  18769  odf1o2  19500  mplcoe5lem  21992  neitr  23122  ordtbas2  23133  ordtopn1  23136  ordtopn2  23137  pnfnei  23162  mnfnei  23163  pnrmcld  23284  2ndcomap  23400  dis2ndc  23402  ptpjopn  23554  fbasrn  23826  elfm  23889  rnelfmlem  23894  rnelfm  23895  fmfnfmlem3  23898  fmfnfmlem4  23899  fmfnfm  23900  ptcmplem2  23995  tsmsfbas  24070  ustuqtoplem  24181  utopsnneiplem  24189  utopsnnei  24191  utopreg  24194  fmucnd  24233  neipcfilu  24237  imasdsf1olem  24315  xpsdsval  24323  met1stc  24463  metustel  24492  metustsym  24497  metuel2  24507  metustbl  24508  restmetu  24512  xrtgioo  24749  minveclem3b  25382  uniioombllem3  25540  dvivth  25969  gausslemma2dlem1a  27330  acunirnmpt  32686  acunirnmpt2  32687  acunirnmpt2f  32688  fnpreimac  32698  trsp2cyc  33154  elrgspnlem1  33273  elrgspnlem2  33274  elrgspn  33277  nsgqusf1olem2  33444  nsgqusf1olem3  33445  locfinreflem  33946  zarclsint  33978  zarcls  33980  ordtconnlem1  34030  esumcst  34169  esumrnmpt2  34174  measdivcstALTV  34331  oms0  34403  omssubadd  34406  cvmsss2  35417  poimirlem16  37776  poimirlem19  37779  poimirlem24  37784  poimirlem27  37787  itg2addnclem2  37812  suprnmpt  45360  rnmptpr  45363  wessf1ornlem  45371  disjrnmpt2  45374  disjf1o  45377  disjinfi  45378  choicefi  45386  rnmptlb  45429  rnmptbddlem  45430  rnmptbd2lem  45434  infnsuprnmpt  45436  elmptima  45444  supxrleubrnmpt  45592  suprleubrnmpt  45608  infrnmptle  45609  infxrunb3rnmpt  45614  supminfrnmpt  45631  infxrgelbrnmpt  45640  infrpgernmpt  45651  supminfxrrnmpt  45657  stoweidlem27  46213  stoweidlem31  46217  stoweidlem35  46221  stirlinglem5  46264  stirlinglem13  46272  fourierdlem80  46372  fourierdlem93  46385  fourierdlem103  46395  fourierdlem104  46396  subsaliuncllem  46543  subsaliuncl  46544  sge0rnn0  46554  sge00  46562  fsumlesge0  46563  sge0tsms  46566  sge0cl  46567  sge0f1o  46568  sge0fsum  46573  sge0supre  46575  sge0rnbnd  46579  sge0pnffigt  46582  sge0lefi  46584  sge0ltfirp  46586  sge0resplit  46592  sge0split  46595  sge0reuz  46633  sge0reuzb  46634  hoidmvlelem2  46782  smfpimcc  46994