Theorem rnmpt 5948

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 5945	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5197	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2792	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5928	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3096	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2836	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2802	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149  {cab 2747  ∃wrex 3095  {copab 5177   ↦ cmpt 5196  ran crn 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-mpt 5197  df-cnv 5670  df-dm 5672  df-rn 5673

This theorem is referenced by:  elrnmpt  5949  elrnmpt1  5951  elrnmptg  5952  dfiun3g  5959  dfiin3g  5960  fnrnfv  6941  fmpt  7106  fnasrn  7142  fliftf  7314  fo1st  8005  fo2nd  8006  fsplitfpar  8112  dfqs2  8700  qliftf  8802  abrexfi  9308  iinfi  9376  tz9.12lem1  9758  infmap2  10199  cfslb2n  10251  fin23lem29  10324  fin23lem30  10325  fin1a2lem11  10393  ac6num  10462  rankcf  10761  tskuni  10767  negfi  12163  4sqlem11  17014  4sqlem12  17015  vdwapval  17032  vdwlem6  17045  quslem  17596  smndex2dnrinv  18976  conjnmzb  19322  pmtrprfvalrn  19557  sylow1lem2  19668  sylow3lem1  19696  sylow3lem2  19697  ablsimpgfind  20181  pzriprnglem10  21608  ellspd  21920  rnascl  22009  iinopn  23027  restco  23289  pnrmopn  23468  cncmp  23517  discmp  23523  comppfsc  23657  alexsublem  24169  ptcmplem3  24179  snclseqg  24241  prdsxmetlem  24493  prdsbl  24616  xrhmeo  25073  pi1xfrf  25180  pi1cof  25186  iunmbl  25680  voliun  25681  itg1addlem4  25826  i1fmulc  25830  mbfi1fseqlem4  25845  itg2monolem1  25877  aannenlem2  26458  2lgslem1b  27521  bdayfo  27806  nosupno  27832  noinfno  27847  addsuniflem  28159  mpteleeOLD  29185  disjrnmpt  32870  ofrn2  32925  abrexct  33000  abrexctf  33002  qusbas2  33658  nsgqusf1olem2  33666  esumc  34385  esumrnmpt  34386  carsgclctunlem3  34654  eulerpartlemt  34705  vonf1oonfo  35497  fobigcup  36288  ptrest  38157  areacirclem2  38247  istotbnd3  38309  sstotbnd  38313  rnasclg  43162  rmxypairf1o  43529  hbtlem6  43747  onsucrn  43889  elrnmptf  45790  fnrnafv  47787  fundcmpsurinjlem1  48035  imasetpreimafvbijlemfo  48042  fargshiftfo  48079