Theorem rnmpt 5980

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 5979	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5250	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2768	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5962	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3077	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2812	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2778	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1537  ∃wex 1777   ∈ wcel 2108  {cab 2717  ∃wrex 3076  {copab 5228   ↦ cmpt 5249  ran crn 5701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-mpt 5250  df-cnv 5708  df-dm 5710  df-rn 5711

This theorem is referenced by:  elrnmpt  5981  elrnmpt1  5983  elrnmptg  5984  dfiun3g  5990  dfiin3g  5991  fnrnfv  6981  fmpt  7144  fnasrn  7179  fliftf  7351  abrexexgOLD  8002  fo1st  8050  fo2nd  8051  fsplitfpar  8159  qliftf  8863  abrexfi  9422  iinfi  9486  tz9.12lem1  9856  infmap2  10286  cfslb2n  10337  fin23lem29  10410  fin23lem30  10411  fin1a2lem11  10479  ac6num  10548  rankcf  10846  tskuni  10852  negfi  12244  4sqlem11  17002  4sqlem12  17003  vdwapval  17020  vdwlem6  17033  quslem  17603  smndex2dnrinv  18950  conjnmzb  19293  pmtrprfvalrn  19530  sylow1lem2  19641  sylow3lem1  19669  sylow3lem2  19670  ablsimpgfind  20154  pzriprnglem10  21524  ellspd  21845  rnascl  21934  iinopn  22929  restco  23193  pnrmopn  23372  cncmp  23421  discmp  23427  comppfsc  23561  alexsublem  24073  ptcmplem3  24083  snclseqg  24145  prdsxmetlem  24399  prdsbl  24525  xrhmeo  24996  pi1xfrf  25105  pi1cof  25111  iunmbl  25607  voliun  25608  itg1addlem4  25753  itg1addlem4OLD  25754  i1fmulc  25758  mbfi1fseqlem4  25773  itg2monolem1  25805  aannenlem2  26389  2lgslem1b  27454  bdayfo  27740  nosupno  27766  noinfno  27781  addsuniflem  28052  mptelee  28928  disjrnmpt  32607  ofrn2  32659  abrexct  32730  abrexctf  32732  qusbas2  33399  nsgqusf1olem2  33407  esumc  34015  esumrnmpt  34016  carsgclctunlem3  34285  eulerpartlemt  34336  fobigcup  35864  ptrest  37579  areacirclem2  37669  istotbnd3  37731  sstotbnd  37735  dfqs2  42232  rnasclg  42454  rmxypairf1o  42868  hbtlem6  43086  onsucrn  43233  elrnmptf  45088  fnrnafv  47077  fundcmpsurinjlem1  47272  imasetpreimafvbijlemfo  47279  fargshiftfo  47316