Theorem rnmpt 5827

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 5826	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5147	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2844	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5807	. 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 1537  ∃wex 1780   ∈ wcel 2114  {cab 2799  ∃wrex 3139  {copab 5128   ↦ cmpt 5146  ran crn 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-mpt 5147  df-cnv 5563  df-dm 5565  df-rn 5566

This theorem is referenced by:  elrnmpt  5828  elrnmpt1  5830  elrnmptg  5831  dfiun3g  5835  dfiin3g  5836  fnrnfv  6725  fmpt  6874  fnasrn  6907  fliftf  7068  abrexexg  7662  fo1st  7709  fo2nd  7710  fsplitfpar  7814  qliftf  8385  abrexfi  8824  iinfi  8881  tz9.12lem1  9216  infmap2  9640  cfslb2n  9690  fin23lem29  9763  fin23lem30  9764  fin1a2lem11  9832  ac6num  9901  rankcf  10199  tskuni  10205  negfi  11589  4sqlem11  16291  4sqlem12  16292  vdwapval  16309  vdwlem6  16322  quslem  16816  smndex2dnrinv  18080  conjnmzb  18393  pmtrprfvalrn  18616  sylow1lem2  18724  sylow3lem1  18752  sylow3lem2  18753  ablsimpgfind  19232  rnascl  20120  ellspd  20946  iinopn  21510  restco  21772  pnrmopn  21951  cncmp  22000  discmp  22006  comppfsc  22140  alexsublem  22652  ptcmplem3  22662  snclseqg  22724  prdsxmetlem  22978  prdsbl  23101  xrhmeo  23550  pi1xfrf  23657  pi1cof  23663  iunmbl  24154  voliun  24155  itg1addlem4  24300  i1fmulc  24304  mbfi1fseqlem4  24319  itg2monolem1  24351  aannenlem2  24918  2lgslem1b  25968  mptelee  26681  disjrnmpt  30335  ofrn2  30387  abrexct  30452  abrexctf  30454  esumc  31310  esumrnmpt  31311  carsgclctunlem3  31578  eulerpartlemt  31629  bdayfo  33182  nosupno  33203  fobigcup  33361  ptrest  34906  areacirclem2  34998  istotbnd3  35064  sstotbnd  35068  dfqs2  39142  rnasclg  39151  rmxypairf1o  39528  hbtlem6  39749  elrnmptf  41461  fnrnafv  43381  fundcmpsurinjlem1  43578  imasetpreimafvbijlemfo  43585  fargshiftfo  43622