Theorem rnmpt 5861

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 5860	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5162	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2767	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5843	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3071	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2809	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2777	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1785   ∈ wcel 2109  {cab 2716  ∃wrex 3066  {copab 5140   ↦ cmpt 5161  ran crn 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-mpt 5162  df-cnv 5596  df-dm 5598  df-rn 5599

This theorem is referenced by:  elrnmpt  5862  elrnmpt1  5864  elrnmptg  5865  dfiun3g  5870  dfiin3g  5871  fnrnfv  6823  fmpt  6978  fnasrn  7011  fliftf  7179  abrexexg  7790  fo1st  7837  fo2nd  7838  fsplitfpar  7943  qliftf  8568  abrexfi  9080  iinfi  9137  tz9.12lem1  9529  infmap2  9958  cfslb2n  10008  fin23lem29  10081  fin23lem30  10082  fin1a2lem11  10150  ac6num  10219  rankcf  10517  tskuni  10523  negfi  11907  4sqlem11  16637  4sqlem12  16638  vdwapval  16655  vdwlem6  16668  quslem  17235  smndex2dnrinv  18535  conjnmzb  18850  pmtrprfvalrn  19077  sylow1lem2  19185  sylow3lem1  19213  sylow3lem2  19214  ablsimpgfind  19694  ellspd  20990  rnascl  21076  iinopn  22032  restco  22296  pnrmopn  22475  cncmp  22524  discmp  22530  comppfsc  22664  alexsublem  23176  ptcmplem3  23186  snclseqg  23248  prdsxmetlem  23502  prdsbl  23628  xrhmeo  24090  pi1xfrf  24197  pi1cof  24203  iunmbl  24698  voliun  24699  itg1addlem4  24844  itg1addlem4OLD  24845  i1fmulc  24849  mbfi1fseqlem4  24864  itg2monolem1  24896  aannenlem2  25470  2lgslem1b  26521  mptelee  27244  disjrnmpt  30903  ofrn2  30956  abrexct  31030  abrexctf  31032  nsgqusf1olem2  31578  esumc  31998  esumrnmpt  31999  carsgclctunlem3  32266  eulerpartlemt  32317  bdayfo  33859  nosupno  33885  noinfno  33900  fobigcup  34181  ptrest  35755  areacirclem2  35845  istotbnd3  35908  sstotbnd  35912  dfqs2  40192  rnasclg  40203  rmxypairf1o  40713  hbtlem6  40934  elrnmptf  42671  fnrnafv  44605  fundcmpsurinjlem1  44802  imasetpreimafvbijlemfo  44809  fargshiftfo  44846