Theorem elrnmpt 5792

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  ∃wrex 3107   ↦ cmpt 5110  ran crn 5520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-mpt 5111  df-cnv 5527  df-dm 5529  df-rn 5530

This theorem is referenced by:  elrnmpt1s  5793  elrnmptd  5797  elrnmptdv  5798  elrnmpt2d  5799  onnseq  7964  oarec  8171  fifo  8880  infpwfien  9473  fin23lem38  9760  fin1a2lem13  9823  ac6num  9890  isercoll2  15017  iserodd  16162  gsumwspan  18003  odf1o2  18690  mplcoe5lem  20707  neitr  21785  ordtbas2  21796  ordtopn1  21799  ordtopn2  21800  pnfnei  21825  mnfnei  21826  pnrmcld  21947  2ndcomap  22063  dis2ndc  22065  ptpjopn  22217  fbasrn  22489  elfm  22552  rnelfmlem  22557  rnelfm  22558  fmfnfmlem3  22561  fmfnfmlem4  22562  fmfnfm  22563  ptcmplem2  22658  tsmsfbas  22733  ustuqtoplem  22845  utopsnneiplem  22853  utopsnnei  22855  utopreg  22858  fmucnd  22898  neipcfilu  22902  imasdsf1olem  22980  xpsdsval  22988  met1stc  23128  metustel  23157  metustsym  23162  metuel2  23172  metustbl  23173  restmetu  23177  xrtgioo  23411  minveclem3b  24032  uniioombllem3  24189  dvivth  24613  gausslemma2dlem1a  25949  elimampt  30397  acunirnmpt  30422  acunirnmpt2  30423  acunirnmpt2f  30424  fnpreimac  30434  trsp2cyc  30815  locfinreflem  31193  zarclsint  31225  zarcls  31227  ordtconnlem1  31277  esumcst  31432  esumrnmpt2  31437  measdivcstALTV  31594  oms0  31665  omssubadd  31668  cvmsss2  32634  poimirlem16  35073  poimirlem19  35076  poimirlem24  35081  poimirlem27  35084  itg2addnclem2  35109  nelrnmpt  41720  suprnmpt  41798  rnmptpr  41801  wessf1ornlem  41811  disjrnmpt2  41815  disjf1o  41818  disjinfi  41820  choicefi  41829  rnmptlb  41880  rnmptbddlem  41881  rnmptbd2lem  41886  infnsuprnmpt  41888  elmptima  41896  supxrleubrnmpt  42043  suprleubrnmpt  42059  infrnmptle  42060  infxrunb3rnmpt  42065  supminfrnmpt  42082  infxrgelbrnmpt  42093  infrpgernmpt  42104  supminfxrrnmpt  42110  stoweidlem27  42669  stoweidlem31  42673  stoweidlem35  42677  stirlinglem5  42720  stirlinglem13  42728  fourierdlem53  42801  fourierdlem80  42828  fourierdlem93  42841  fourierdlem103  42851  fourierdlem104  42852  subsaliuncllem  42997  subsaliuncl  42998  sge0rnn0  43007  sge00  43015  fsumlesge0  43016  sge0tsms  43019  sge0cl  43020  sge0f1o  43021  sge0fsum  43026  sge0supre  43028  sge0rnbnd  43032  sge0pnffigt  43035  sge0lefi  43037  sge0ltfirp  43039  sge0resplit  43045  sge0split  43048  sge0reuz  43086  sge0reuzb  43087  hoidmvlelem2  43235  smfpimcc  43439