Theorem dmmptg 6193

Description: The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013.) (Revised by Mario Carneiro, 14-Sep-2013.)

Assertion

Ref	Expression
dmmptg	⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem dmmptg

Step	Hyp	Ref	Expression
1		eqid 2739	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6191	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3452	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3076	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3424	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 235	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2793	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ∀wral 3053  {crab 3391  Vcvv 3431   ↦ cmpt 5153  dom cdm 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-mpt 5154  df-xp 5624  df-rel 5625  df-cnv 5626  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631

This theorem is referenced by:  rnmpt0f  6194  ovmpt3rabdm  7615  suppssov1  8137  suppssov2  8138  suppssfv  8142  iinon  8270  onoviun  8273  noinfep  9572  cantnfdm  9576  axcc2lem  10349  negfi  12096  ccatalpha  14547  swrd0  14612  o1lo1  15490  o1lo12  15491  lo1mptrcl  15575  o1mptrcl  15576  o1add2  15577  o1mul2  15578  o1sub2  15579  lo1add  15580  lo1mul  15581  o1dif  15583  rlimneg  15600  lo1le  15605  rlimno1  15607  o1fsum  15767  divsfval  17502  subdrgint  20775  iscnp2  23222  ptcnplem  23604  xkoinjcn  23670  fbasrn  23867  prdsdsf  24350  ressprdsds  24354  mbfmptcl  25621  mbfdm2  25622  dvmptresicc  25901  dvmptcl  25944  dvmptadd  25945  dvmptmul  25946  dvmptres2  25947  dvmptcmul  25949  dvmptcj  25953  dvmptco  25957  rolle  25975  dvlip  25978  dvlipcn  25979  dvle  25992  dvivthlem1  25993  dvivth  25995  dvfsumle  26006  dvfsumge  26007  dvmptrecl  26009  dvfsumlem2  26012  pserdv  26412  logtayl  26642  relogbf  26773  rlimcxp  26955  o1cxp  26956  gsummpt2co  33129  psgnfzto1stlem  33181  measdivcstALTV  34409  probfinmeasbALTV  34613  probmeasb  34614  dstrvprob  34656  cvmsss2  35502  sdclem2  38109  3factsumint1  42506  dmmzp  43182  dvcosax  46369  dvnprodlem3  46391  itgcoscmulx  46412  stoweidlem27  46470  dirkeritg  46545  fourierdlem16  46566  fourierdlem21  46571  fourierdlem22  46572  fourierdlem39  46589  fourierdlem57  46606  fourierdlem58  46607  fourierdlem60  46609  fourierdlem61  46610  fourierdlem73  46622  fourierdlem83  46632  subsaliuncllem  46800  0ome  46972  hoi2toco  47050  elbigofrcl  49041  itcoval0mpt  49157