Theorem elrnmpt 5900

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3053   ↦ cmpt 5173  ran crn 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-mpt 5174  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  elrnmpt1s  5901  elrnmptd  5905  elrnmptdv  5907  elrnmpt2d  5908  elimampt  5994  onnseq  8267  oarec  8480  fifo  9322  infpwfien  9956  fin23lem38  10243  fin1a2lem13  10306  ac6num  10373  isercoll2  15576  iserodd  16747  gsumwspan  18720  odf1o2  19452  mplcoe5lem  21944  neitr  23065  ordtbas2  23076  ordtopn1  23079  ordtopn2  23080  pnfnei  23105  mnfnei  23106  pnrmcld  23227  2ndcomap  23343  dis2ndc  23345  ptpjopn  23497  fbasrn  23769  elfm  23832  rnelfmlem  23837  rnelfm  23838  fmfnfmlem3  23841  fmfnfmlem4  23842  fmfnfm  23843  ptcmplem2  23938  tsmsfbas  24013  ustuqtoplem  24125  utopsnneiplem  24133  utopsnnei  24135  utopreg  24138  fmucnd  24177  neipcfilu  24181  imasdsf1olem  24259  xpsdsval  24267  met1stc  24407  metustel  24436  metustsym  24441  metuel2  24451  metustbl  24452  restmetu  24456  xrtgioo  24693  minveclem3b  25326  uniioombllem3  25484  dvivth  25913  gausslemma2dlem1a  27274  acunirnmpt  32603  acunirnmpt2  32604  acunirnmpt2f  32605  fnpreimac  32615  trsp2cyc  33066  elrgspnlem1  33183  elrgspnlem2  33184  elrgspn  33187  nsgqusf1olem2  33352  nsgqusf1olem3  33353  locfinreflem  33813  zarclsint  33845  zarcls  33847  ordtconnlem1  33897  esumcst  34036  esumrnmpt2  34041  measdivcstALTV  34198  oms0  34271  omssubadd  34274  cvmsss2  35257  poimirlem16  37626  poimirlem19  37629  poimirlem24  37634  poimirlem27  37637  itg2addnclem2  37662  nelrnmpt  45072  suprnmpt  45162  rnmptpr  45165  wessf1ornlem  45173  disjrnmpt2  45176  disjf1o  45179  disjinfi  45180  choicefi  45188  rnmptlb  45231  rnmptbddlem  45232  rnmptbd2lem  45236  infnsuprnmpt  45238  elmptima  45246  supxrleubrnmpt  45395  suprleubrnmpt  45411  infrnmptle  45412  infxrunb3rnmpt  45417  supminfrnmpt  45434  infxrgelbrnmpt  45443  infrpgernmpt  45454  supminfxrrnmpt  45460  stoweidlem27  46018  stoweidlem31  46022  stoweidlem35  46026  stirlinglem5  46069  stirlinglem13  46077  fourierdlem80  46177  fourierdlem93  46190  fourierdlem103  46200  fourierdlem104  46201  subsaliuncllem  46348  subsaliuncl  46349  sge0rnn0  46359  sge00  46367  fsumlesge0  46368  sge0tsms  46371  sge0cl  46372  sge0f1o  46373  sge0fsum  46378  sge0supre  46380  sge0rnbnd  46384  sge0pnffigt  46387  sge0lefi  46389  sge0ltfirp  46391  sge0resplit  46397  sge0split  46400  sge0reuz  46438  sge0reuzb  46439  hoidmvlelem2  46587  smfpimcc  46799