Theorem elrnmpt 5372

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   ∈ wcel 1990  ∃wrex 2913   ↦ cmpt 4729  ran crn 5115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-mpt 4730  df-cnv 5122  df-dm 5124  df-rn 5125

This theorem is referenced by:  elrnmpt1s  5373  onnseq  7441  oarec  7642  fifo  8338  infpwfien  8885  fin23lem38  9171  fin1a2lem13  9234  ac6num  9301  isercoll2  14399  iserodd  15540  gsumwspan  17383  odf1o2  17988  mplcoe5lem  19467  neitr  20984  ordtbas2  20995  ordtopn1  20998  ordtopn2  20999  pnfnei  21024  mnfnei  21025  pnrmcld  21146  2ndcomap  21261  dis2ndc  21263  ptpjopn  21415  fbasrn  21688  elfm  21751  rnelfmlem  21756  rnelfm  21757  fmfnfmlem3  21760  fmfnfmlem4  21761  fmfnfm  21762  ptcmplem2  21857  tsmsfbas  21931  ustuqtoplem  22043  utopsnneiplem  22051  utopsnnei  22053  utopreg  22056  fmucnd  22096  neipcfilu  22100  imasdsf1olem  22178  xpsdsval  22186  met1stc  22326  metustel  22355  metustsym  22360  metuel2  22370  metustbl  22371  restmetu  22375  xrtgioo  22609  minveclem3b  23199  uniioombllem3  23353  dvivth  23773  gausslemma2dlem1a  25090  elimampt  29438  acunirnmpt  29459  acunirnmpt2  29460  acunirnmpt2f  29461  locfinreflem  29907  ordtconnlem1  29970  esumcst  30125  esumrnmpt2  30130  measdivcstOLD  30287  oms0  30359  omssubadd  30362  cvmsss2  31256  poimirlem16  33425  poimirlem19  33428  poimirlem24  33433  poimirlem27  33436  itg2addnclem2  33462  nelrnmpt  39257  suprnmpt  39355  rnmptpr  39358  elrnmptd  39366  rnmptssrn  39368  wessf1ornlem  39371  disjrnmpt2  39375  disjf1o  39378  disjinfi  39380  choicefi  39392  rnmptlb  39453  rnmptbddlem  39455  rnmptbd2lem  39463  infnsuprnmpt  39465  elmptima  39473  supxrleubrnmpt  39632  suprleubrnmpt  39649  infrnmptle  39650  infxrunb3rnmpt  39655  supminfrnmpt  39672  infxrgelbrnmpt  39683  infrpgernmpt  39695  supminfxrrnmpt  39701  stoweidlem27  40244  stoweidlem31  40248  stoweidlem35  40252  stirlinglem5  40295  stirlinglem13  40303  fourierdlem53  40376  fourierdlem80  40403  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  subsaliuncllem  40575  subsaliuncl  40576  sge0rnn0  40585  sge00  40593  fsumlesge0  40594  sge0tsms  40597  sge0cl  40598  sge0f1o  40599  sge0fsum  40604  sge0supre  40606  sge0rnbnd  40610  sge0pnffigt  40613  sge0lefi  40615  sge0ltfirp  40617  sge0resplit  40623  sge0split  40626  sge0reuz  40664  sge0reuzb  40665  hoidmvlelem2  40810  smfpimcc  41014