Theorem elrnmpt 5897

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  ∃wrex 3056   ↦ cmpt 5170  ran crn 5615

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-mpt 5171  df-cnv 5622  df-dm 5624  df-rn 5625

This theorem is referenced by:  elrnmpt1s  5898  elrnmptd  5902  elrnmptdv  5904  elrnmpt2d  5905  elimampt  5991  onnseq  8264  oarec  8477  fifo  9316  infpwfien  9953  fin23lem38  10240  fin1a2lem13  10303  ac6num  10370  isercoll2  15576  iserodd  16747  gsumwspan  18754  odf1o2  19485  mplcoe5lem  21974  neitr  23095  ordtbas2  23106  ordtopn1  23109  ordtopn2  23110  pnfnei  23135  mnfnei  23136  pnrmcld  23257  2ndcomap  23373  dis2ndc  23375  ptpjopn  23527  fbasrn  23799  elfm  23862  rnelfmlem  23867  rnelfm  23868  fmfnfmlem3  23871  fmfnfmlem4  23872  fmfnfm  23873  ptcmplem2  23968  tsmsfbas  24043  ustuqtoplem  24154  utopsnneiplem  24162  utopsnnei  24164  utopreg  24167  fmucnd  24206  neipcfilu  24210  imasdsf1olem  24288  xpsdsval  24296  met1stc  24436  metustel  24465  metustsym  24470  metuel2  24480  metustbl  24481  restmetu  24485  xrtgioo  24722  minveclem3b  25355  uniioombllem3  25513  dvivth  25942  gausslemma2dlem1a  27303  acunirnmpt  32641  acunirnmpt2  32642  acunirnmpt2f  32643  fnpreimac  32653  trsp2cyc  33092  elrgspnlem1  33209  elrgspnlem2  33210  elrgspn  33213  nsgqusf1olem2  33379  nsgqusf1olem3  33380  locfinreflem  33853  zarclsint  33885  zarcls  33887  ordtconnlem1  33937  esumcst  34076  esumrnmpt2  34081  measdivcstALTV  34238  oms0  34310  omssubadd  34313  cvmsss2  35318  poimirlem16  37675  poimirlem19  37678  poimirlem24  37683  poimirlem27  37686  itg2addnclem2  37711  nelrnmpt  45180  suprnmpt  45270  rnmptpr  45273  wessf1ornlem  45281  disjrnmpt2  45284  disjf1o  45287  disjinfi  45288  choicefi  45296  rnmptlb  45339  rnmptbddlem  45340  rnmptbd2lem  45344  infnsuprnmpt  45346  elmptima  45354  supxrleubrnmpt  45503  suprleubrnmpt  45519  infrnmptle  45520  infxrunb3rnmpt  45525  supminfrnmpt  45542  infxrgelbrnmpt  45551  infrpgernmpt  45562  supminfxrrnmpt  45568  stoweidlem27  46124  stoweidlem31  46128  stoweidlem35  46132  stirlinglem5  46175  stirlinglem13  46183  fourierdlem80  46283  fourierdlem93  46296  fourierdlem103  46306  fourierdlem104  46307  subsaliuncllem  46454  subsaliuncl  46455  sge0rnn0  46465  sge00  46473  fsumlesge0  46474  sge0tsms  46477  sge0cl  46478  sge0f1o  46479  sge0fsum  46484  sge0supre  46486  sge0rnbnd  46490  sge0pnffigt  46493  sge0lefi  46495  sge0ltfirp  46497  sge0resplit  46503  sge0split  46506  sge0reuz  46544  sge0reuzb  46545  hoidmvlelem2  46693  smfpimcc  46905