Theorem rnmpt 5951

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 5948	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5193	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2786	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5931	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3091	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2830	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2796	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2147  {cab 2741  ∃wrex 3090  {copab 5173   ↦ cmpt 5192  ran crn 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-mpt 5193  df-cnv 5666  df-dm 5668  df-rn 5669

This theorem is used by:  elrnmpt  5952  elrnmpt1  5954  elrnmptg  5955  dfiun3g  5962  dfiin3g  5963  fnrnfv  6975  fmpt  7142  fnasrn  7180  fliftf  7354  fo1st  8055  fo2nd  8056  fsplitfpar  8166  dfqs2  8762  qliftf  8864  abrexfi  9379  iinfi  9446  tz9.12lem1  9831  infmap2  10334  cfslb2n  10385  fin23lem29  10458  fin23lem30  10459  fin1a2lem11  10527  ac6num  10596  rankcf  10901  tskuni  10907  negfi  12306  4sqlem11  17177  4sqlem12  17178  vdwapval  17195  vdwlem6  17208  quslem  17765  smndex2dnrinv  19164  conjnmzb  19517  pmtrprfvalrn  19753  sylow1lem2  19864  sylow3lem1  19892  sylow3lem2  19893  ablsimpgfind  20377  pzriprnglem10  21851  ellspd  22163  rnascl  22254  iinopn  23275  restco  23537  pnrmopn  23716  cncmp  23765  discmp  23771  abrexct  23828  comppfsc  23906  alexsublem  24418  ptcmplem3  24428  snclseqg  24490  prdsxmetlem  24742  prdsbl  24865  xrhmeo  25322  pi1xfrf  25429  pi1cof  25435  iunmbl  25929  voliun  25930  itg1addlem4  26075  i1fmulc  26079  mbfi1fseqlem4  26094  itg2monolem1  26126  aannenlem2  26713  2lgslem1b  27776  bdayfo  28091  nosupno  28117  noinfno  28132  addsuniflem  28444  mpteleeOLD  29530  disjrnmpt  33277  ofrn2  33332  abrexctf  33406  qusbas2  34061  nsgqusf1olem2  34069  esumc  34794  esumrnmpt  34795  carsgclctunlem3  35063  eulerpartlemt  35114  jf1o  36052  vonf1oonfo  36090  fobigcup  36877  ptrest  38805  areacirclem2  38895  istotbnd3  38971  sstotbnd  38975  rnasclg  43829  rmxypairf1o  44184  hbtlem6  44396  onsucrn  44534  elrnmptf  46469  omeiunle  47800  fnrnafv  48505  fundcmpsurinjlem1  48753  imasetpreimafvbijlemfo  48760  fargshiftfo  48797