Theorem elrnmpt 5911

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

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

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-mpt 5184  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  elrnmpt1s  5912  elrnmptd  5916  elrnmptdv  5918  elrnmpt2d  5919  elimampt  6003  onnseq  8290  oarec  8503  fifo  9359  infpwfien  9991  fin23lem38  10278  fin1a2lem13  10341  ac6num  10408  isercoll2  15611  iserodd  16782  gsumwspan  18755  odf1o2  19487  mplcoe5lem  21979  neitr  23100  ordtbas2  23111  ordtopn1  23114  ordtopn2  23115  pnfnei  23140  mnfnei  23141  pnrmcld  23262  2ndcomap  23378  dis2ndc  23380  ptpjopn  23532  fbasrn  23804  elfm  23867  rnelfmlem  23872  rnelfm  23873  fmfnfmlem3  23876  fmfnfmlem4  23877  fmfnfm  23878  ptcmplem2  23973  tsmsfbas  24048  ustuqtoplem  24160  utopsnneiplem  24168  utopsnnei  24170  utopreg  24173  fmucnd  24212  neipcfilu  24216  imasdsf1olem  24294  xpsdsval  24302  met1stc  24442  metustel  24471  metustsym  24476  metuel2  24486  metustbl  24487  restmetu  24491  xrtgioo  24728  minveclem3b  25361  uniioombllem3  25519  dvivth  25948  gausslemma2dlem1a  27309  acunirnmpt  32633  acunirnmpt2  32634  acunirnmpt2f  32635  fnpreimac  32645  trsp2cyc  33095  elrgspnlem1  33209  elrgspnlem2  33210  elrgspn  33213  nsgqusf1olem2  33378  nsgqusf1olem3  33379  locfinreflem  33823  zarclsint  33855  zarcls  33857  ordtconnlem1  33907  esumcst  34046  esumrnmpt2  34051  measdivcstALTV  34208  oms0  34281  omssubadd  34284  cvmsss2  35254  poimirlem16  37623  poimirlem19  37626  poimirlem24  37631  poimirlem27  37634  itg2addnclem2  37659  nelrnmpt  45071  suprnmpt  45161  rnmptpr  45164  wessf1ornlem  45172  disjrnmpt2  45175  disjf1o  45178  disjinfi  45179  choicefi  45187  rnmptlb  45230  rnmptbddlem  45231  rnmptbd2lem  45235  infnsuprnmpt  45237  elmptima  45245  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