Theorem rnmpt 5403

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 5402	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 4763	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2673	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5384	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 2947	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2768	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2683	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 383   = wceq 1523  ∃wex 1744   ∈ wcel 2030  {cab 2637  ∃wrex 2942  {copab 4745   ↦ cmpt 4762  ran crn 5144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-mpt 4763  df-cnv 5151  df-dm 5153  df-rn 5154

This theorem is referenced by:  elrnmpt  5404  elrnmpt1  5406  elrnmptg  5407  dfiun3g  5410  dfiin3g  5411  fnrnfv  6281  fmpt  6421  fnasrn  6451  fliftf  6605  abrexexg  7182  abrexexOLD  7184  fo1st  7230  fo2nd  7231  qliftf  7878  abrexfi  8307  iinfi  8364  tz9.12lem1  8688  infmap2  9078  cfslb2n  9128  fin23lem29  9201  fin23lem30  9202  fin1a2lem11  9270  ac6num  9339  rankcf  9637  tskuni  9643  negfi  11009  4sqlem11  15706  4sqlem12  15707  vdwapval  15724  vdwlem6  15737  quslem  16250  conjnmzb  17742  pmtrprfvalrn  17954  sylow1lem2  18060  sylow3lem1  18088  sylow3lem2  18089  rnascl  19391  ellspd  20189  iinopn  20755  restco  21016  pnrmopn  21195  cncmp  21243  discmp  21249  comppfsc  21383  alexsublem  21895  ptcmplem3  21905  snclseqg  21966  prdsxmetlem  22220  prdsbl  22343  xrhmeo  22792  pi1xfrf  22899  pi1cof  22905  iunmbl  23367  voliun  23368  itg1addlem4  23511  i1fmulc  23515  mbfi1fseqlem4  23530  itg2monolem1  23562  aannenlem2  24129  2lgslem1b  25162  mptelee  25820  disjrnmpt  29524  ofrn2  29570  abrexct  29622  abrexctf  29624  esumc  30241  esumrnmpt  30242  carsgclctunlem3  30510  eulerpartlemt  30561  bdayfo  31953  nosupno  31974  fobigcup  32132  ptrest  33538  areacirclem2  33631  istotbnd3  33700  sstotbnd  33704  rmxypairf1o  37793  hbtlem6  38016  elrnmptf  39681  fnrnafv  41563  fargshiftfo  41703