Theorem rnmpt 5907

Description: The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)

Hypothesis

Ref	Expression
rnmpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
rnmpt	⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐹(𝑥,𝑦)

Proof of Theorem rnmpt

Step	Hyp	Ref	Expression
1		rnopab 5904	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5168	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2760	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5887	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3063	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2804	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2770	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715  ∃wrex 3062  {copab 5148   ↦ cmpt 5167  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 5232  ax-pr 5371

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 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  elrnmpt  5908  elrnmpt1  5910  elrnmptg  5911  dfiun3g  5918  dfiin3g  5919  fnrnfv  6894  fmpt  7057  fnasrn  7093  fliftf  7264  fo1st  7956  fo2nd  7957  fsplitfpar  8062  dfqs2  8644  qliftf  8746  abrexfi  9256  iinfi  9324  tz9.12lem1  9705  infmap2  10133  cfslb2n  10184  fin23lem29  10257  fin23lem30  10258  fin1a2lem11  10326  ac6num  10395  rankcf  10694  tskuni  10700  negfi  12099  4sqlem11  16920  4sqlem12  16921  vdwapval  16938  vdwlem6  16951  quslem  17501  smndex2dnrinv  18880  conjnmzb  19222  pmtrprfvalrn  19457  sylow1lem2  19568  sylow3lem1  19596  sylow3lem2  19597  ablsimpgfind  20081  pzriprnglem10  21483  ellspd  21795  rnascl  21884  iinopn  22880  restco  23142  pnrmopn  23321  cncmp  23370  discmp  23376  comppfsc  23510  alexsublem  24022  ptcmplem3  24032  snclseqg  24094  prdsxmetlem  24346  prdsbl  24469  xrhmeo  24926  pi1xfrf  25033  pi1cof  25039  iunmbl  25533  voliun  25534  itg1addlem4  25679  i1fmulc  25683  mbfi1fseqlem4  25698  itg2monolem1  25730  aannenlem2  26309  2lgslem1b  27372  bdayfo  27658  nosupno  27684  noinfno  27699  addsuniflem  28010  mpteleeOLD  28981  disjrnmpt  32673  ofrn2  32731  abrexct  32806  abrexctf  32808  qusbas2  33484  nsgqusf1olem2  33492  esumc  34214  esumrnmpt  34215  carsgclctunlem3  34483  eulerpartlemt  34534  fobigcup  36099  ptrest  37957  areacirclem2  38047  istotbnd3  38109  sstotbnd  38113  rnasclg  42961  rmxypairf1o  43360  hbtlem6  43578  onsucrn  43720  elrnmptf  45632  fnrnafv  47625  fundcmpsurinjlem1  47873  imasetpreimafvbijlemfo  47880  fargshiftfo  47917