Theorem elrnmpt 5672

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507   ∈ wcel 2050  ∃wrex 3089   ↦ cmpt 5009  ran crn 5409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pr 5187

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-op 4449  df-br 4931  df-opab 4993  df-mpt 5010  df-cnv 5416  df-dm 5418  df-rn 5419

This theorem is referenced by:  elrnmpt1s  5673  onnseq  7787  oarec  7991  fifo  8693  infpwfien  9284  fin23lem38  9571  fin1a2lem13  9634  ac6num  9701  isercoll2  14889  iserodd  16031  gsumwspan  17855  odf1o2  18462  mplcoe5lem  19964  neitr  21495  ordtbas2  21506  ordtopn1  21509  ordtopn2  21510  pnfnei  21535  mnfnei  21536  pnrmcld  21657  2ndcomap  21773  dis2ndc  21775  ptpjopn  21927  fbasrn  22199  elfm  22262  rnelfmlem  22267  rnelfm  22268  fmfnfmlem3  22271  fmfnfmlem4  22272  fmfnfm  22273  ptcmplem2  22368  tsmsfbas  22442  ustuqtoplem  22554  utopsnneiplem  22562  utopsnnei  22564  utopreg  22567  fmucnd  22607  neipcfilu  22611  imasdsf1olem  22689  xpsdsval  22697  met1stc  22837  metustel  22866  metustsym  22871  metuel2  22881  metustbl  22882  restmetu  22886  xrtgioo  23120  minveclem3b  23737  uniioombllem3  23892  dvivth  24313  gausslemma2dlem1a  25646  elimampt  30148  acunirnmpt  30169  acunirnmpt2  30170  acunirnmpt2f  30171  fnpreimac  30181  locfinreflem  30748  ordtconnlem1  30811  esumcst  30966  esumrnmpt2  30971  measdivcstOLD  31128  oms0  31200  omssubadd  31203  cvmsss2  32106  poimirlem16  34349  poimirlem19  34352  poimirlem24  34357  poimirlem27  34360  itg2addnclem2  34385  rr-elrnmptd  39926  rr-elrnmpt2d  39927  nelrnmpt  40768  suprnmpt  40855  rnmptpr  40858  elrnmptd  40865  wessf1ornlem  40870  disjrnmpt2  40874  disjf1o  40877  disjinfi  40879  choicefi  40889  rnmptlb  40942  rnmptbddlem  40943  rnmptbd2lem  40949  infnsuprnmpt  40951  elmptima  40959  supxrleubrnmpt  41111  suprleubrnmpt  41128  infrnmptle  41129  infxrunb3rnmpt  41134  supminfrnmpt  41151  infxrgelbrnmpt  41162  infrpgernmpt  41173  supminfxrrnmpt  41179  stoweidlem27  41744  stoweidlem31  41748  stoweidlem35  41752  stirlinglem5  41795  stirlinglem13  41803  fourierdlem53  41876  fourierdlem80  41903  fourierdlem93  41916  fourierdlem103  41926  fourierdlem104  41927  subsaliuncllem  42072  subsaliuncl  42073  sge0rnn0  42082  sge00  42090  fsumlesge0  42091  sge0tsms  42094  sge0cl  42095  sge0f1o  42096  sge0fsum  42101  sge0supre  42103  sge0rnbnd  42107  sge0pnffigt  42110  sge0lefi  42112  sge0ltfirp  42114  sge0resplit  42120  sge0split  42123  sge0reuz  42161  sge0reuzb  42162  hoidmvlelem2  42310  smfpimcc  42514