Theorem elrnmpt 5908

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3061   ↦ cmpt 5180  ran crn 5626

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-mpt 5181  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  elrnmpt1s  5909  elrnmptd  5913  elrnmptdv  5915  elrnmpt2d  5916  nelrnmpt  5917  elimampt  6003  onnseq  8278  oarec  8491  fifo  9339  infpwfien  9976  fin23lem38  10263  fin1a2lem13  10326  ac6num  10393  isercoll2  15596  iserodd  16767  gsumwspan  18775  odf1o2  19506  mplcoe5lem  21998  neitr  23128  ordtbas2  23139  ordtopn1  23142  ordtopn2  23143  pnfnei  23168  mnfnei  23169  pnrmcld  23290  2ndcomap  23406  dis2ndc  23408  ptpjopn  23560  fbasrn  23832  elfm  23895  rnelfmlem  23900  rnelfm  23901  fmfnfmlem3  23904  fmfnfmlem4  23905  fmfnfm  23906  ptcmplem2  24001  tsmsfbas  24076  ustuqtoplem  24187  utopsnneiplem  24195  utopsnnei  24197  utopreg  24200  fmucnd  24239  neipcfilu  24243  imasdsf1olem  24321  xpsdsval  24329  met1stc  24469  metustel  24498  metustsym  24503  metuel2  24513  metustbl  24514  restmetu  24518  xrtgioo  24755  minveclem3b  25388  uniioombllem3  25546  dvivth  25975  gausslemma2dlem1a  27336  acunirnmpt  32740  acunirnmpt2  32741  acunirnmpt2f  32742  fnpreimac  32751  trsp2cyc  33207  elrgspnlem1  33326  elrgspnlem2  33327  elrgspn  33330  nsgqusf1olem2  33497  nsgqusf1olem3  33498  locfinreflem  33999  zarclsint  34031  zarcls  34033  ordtconnlem1  34083  esumcst  34222  esumrnmpt2  34227  measdivcstALTV  34384  oms0  34456  omssubadd  34459  cvmsss2  35470  poimirlem16  37839  poimirlem19  37842  poimirlem24  37847  poimirlem27  37850  itg2addnclem2  37875  suprnmpt  45485  rnmptpr  45488  wessf1ornlem  45496  disjrnmpt2  45499  disjf1o  45502  disjinfi  45503  choicefi  45511  rnmptlb  45554  rnmptbddlem  45555  rnmptbd2lem  45559  infnsuprnmpt  45561  elmptima  45569  supxrleubrnmpt  45717  suprleubrnmpt  45733  infrnmptle  45734  infxrunb3rnmpt  45739  supminfrnmpt  45756  infxrgelbrnmpt  45765  infrpgernmpt  45776  supminfxrrnmpt  45782  stoweidlem27  46338  stoweidlem31  46342  stoweidlem35  46346  stirlinglem5  46389  stirlinglem13  46397  fourierdlem80  46497  fourierdlem93  46510  fourierdlem103  46520  fourierdlem104  46521  subsaliuncllem  46668  subsaliuncl  46669  sge0rnn0  46679  sge00  46687  fsumlesge0  46688  sge0tsms  46691  sge0cl  46692  sge0f1o  46693  sge0fsum  46698  sge0supre  46700  sge0rnbnd  46704  sge0pnffigt  46707  sge0lefi  46709  sge0ltfirp  46711  sge0resplit  46717  sge0split  46720  sge0reuz  46758  sge0reuzb  46759  hoidmvlelem2  46907  smfpimcc  47119