Theorem rnmpt 5971

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 5968	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5232	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2763	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5951	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3069	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2807	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2773	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1537  ∃wex 1776   ∈ wcel 2106  {cab 2712  ∃wrex 3068  {copab 5210   ↦ cmpt 5231  ran crn 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-mpt 5232  df-cnv 5697  df-dm 5699  df-rn 5700

This theorem is referenced by:  elrnmpt  5972  elrnmpt1  5974  elrnmptg  5975  dfiun3g  5981  dfiin3g  5982  fnrnfv  6968  fmpt  7130  fnasrn  7165  fliftf  7335  abrexexgOLD  7985  fo1st  8033  fo2nd  8034  fsplitfpar  8142  qliftf  8844  abrexfi  9390  iinfi  9455  tz9.12lem1  9825  infmap2  10255  cfslb2n  10306  fin23lem29  10379  fin23lem30  10380  fin1a2lem11  10448  ac6num  10517  rankcf  10815  tskuni  10821  negfi  12215  4sqlem11  16989  4sqlem12  16990  vdwapval  17007  vdwlem6  17020  quslem  17590  smndex2dnrinv  18941  conjnmzb  19284  pmtrprfvalrn  19521  sylow1lem2  19632  sylow3lem1  19660  sylow3lem2  19661  ablsimpgfind  20145  pzriprnglem10  21519  ellspd  21840  rnascl  21929  iinopn  22924  restco  23188  pnrmopn  23367  cncmp  23416  discmp  23422  comppfsc  23556  alexsublem  24068  ptcmplem3  24078  snclseqg  24140  prdsxmetlem  24394  prdsbl  24520  xrhmeo  24991  pi1xfrf  25100  pi1cof  25106  iunmbl  25602  voliun  25603  itg1addlem4  25748  itg1addlem4OLD  25749  i1fmulc  25753  mbfi1fseqlem4  25768  itg2monolem1  25800  aannenlem2  26386  2lgslem1b  27451  bdayfo  27737  nosupno  27763  noinfno  27778  addsuniflem  28049  mptelee  28925  disjrnmpt  32605  ofrn2  32657  abrexct  32734  abrexctf  32736  qusbas2  33414  nsgqusf1olem2  33422  esumc  34032  esumrnmpt  34033  carsgclctunlem3  34302  eulerpartlemt  34353  fobigcup  35882  ptrest  37606  areacirclem2  37696  istotbnd3  37758  sstotbnd  37762  dfqs2  42257  rnasclg  42486  rmxypairf1o  42900  hbtlem6  43118  onsucrn  43261  elrnmptf  45124  fnrnafv  47112  fundcmpsurinjlem1  47323  imasetpreimafvbijlemfo  47330  fargshiftfo  47367