Theorem rnmpt 5826

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 5825	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5146	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2844	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5806	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3144	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2886	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2854	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 398   = wceq 1533  ∃wex 1776   ∈ wcel 2110  {cab 2799  ∃wrex 3139  {copab 5127   ↦ cmpt 5145  ran crn 5555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-br 5066  df-opab 5128  df-mpt 5146  df-cnv 5562  df-dm 5564  df-rn 5565

This theorem is referenced by:  elrnmpt  5827  elrnmpt1  5829  elrnmptg  5830  dfiun3g  5834  dfiin3g  5835  fnrnfv  6724  fmpt  6873  fnasrn  6906  fliftf  7067  abrexexg  7661  fo1st  7708  fo2nd  7709  fsplitfpar  7813  qliftf  8384  abrexfi  8823  iinfi  8880  tz9.12lem1  9215  infmap2  9639  cfslb2n  9689  fin23lem29  9762  fin23lem30  9763  fin1a2lem11  9831  ac6num  9900  rankcf  10198  tskuni  10204  negfi  11588  4sqlem11  16290  4sqlem12  16291  vdwapval  16308  vdwlem6  16321  quslem  16815  smndex2dnrinv  18079  conjnmzb  18392  pmtrprfvalrn  18615  sylow1lem2  18723  sylow3lem1  18751  sylow3lem2  18752  ablsimpgfind  19231  rnascl  20119  ellspd  20945  iinopn  21509  restco  21771  pnrmopn  21950  cncmp  21999  discmp  22005  comppfsc  22139  alexsublem  22651  ptcmplem3  22661  snclseqg  22723  prdsxmetlem  22977  prdsbl  23100  xrhmeo  23549  pi1xfrf  23656  pi1cof  23662  iunmbl  24153  voliun  24154  itg1addlem4  24299  i1fmulc  24303  mbfi1fseqlem4  24318  itg2monolem1  24350  aannenlem2  24917  2lgslem1b  25967  mptelee  26680  disjrnmpt  30334  ofrn2  30386  abrexct  30451  abrexctf  30453  esumc  31310  esumrnmpt  31311  carsgclctunlem3  31578  eulerpartlemt  31629  bdayfo  33182  nosupno  33203  fobigcup  33361  ptrest  34890  areacirclem2  34982  istotbnd3  35048  sstotbnd  35052  dfqs2  39120  rnasclg  39129  rmxypairf1o  39506  hbtlem6  39727  elrnmptf  41439  fnrnafv  43360  fundcmpsurinjlem1  43557  imasetpreimafvbijlemfo  43564  fargshiftfo  43601