Theorem dmmptg 6206

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 2736	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6204	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3450	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3074	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3422	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 234	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2790	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3051  {crab 3389  Vcvv 3429   ↦ cmpt 5166  dom cdm 5631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-mpt 5167  df-xp 5637  df-rel 5638  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  rnmpt0f  6207  ovmpt3rabdm  7626  suppssov1  8147  suppssov2  8148  suppssfv  8152  iinon  8280  onoviun  8283  noinfep  9581  cantnfdm  9585  axcc2lem  10358  negfi  12105  ccatalpha  14556  swrd0  14621  o1lo1  15499  o1lo12  15500  lo1mptrcl  15584  o1mptrcl  15585  o1add2  15586  o1mul2  15587  o1sub2  15588  lo1add  15589  lo1mul  15590  o1dif  15592  rlimneg  15609  lo1le  15614  rlimno1  15616  o1fsum  15776  divsfval  17511  subdrgint  20780  iscnp2  23204  ptcnplem  23586  xkoinjcn  23652  fbasrn  23849  prdsdsf  24332  ressprdsds  24336  mbfmptcl  25603  mbfdm2  25604  dvmptresicc  25883  dvmptcl  25926  dvmptadd  25927  dvmptmul  25928  dvmptres2  25929  dvmptcmul  25931  dvmptcj  25935  dvmptco  25939  rolle  25957  dvlip  25960  dvlipcn  25961  dvle  25974  dvivthlem1  25975  dvivth  25977  dvfsumle  25988  dvfsumge  25989  dvmptrecl  25991  dvfsumlem2  25994  pserdv  26394  logtayl  26624  relogbf  26755  rlimcxp  26937  o1cxp  26938  gsummpt2co  33109  psgnfzto1stlem  33161  measdivcstALTV  34369  probfinmeasbALTV  34573  probmeasb  34574  dstrvprob  34616  cvmsss2  35456  sdclem2  38063  3factsumint1  42460  dmmzp  43165  dvcosax  46354  dvnprodlem3  46376  itgcoscmulx  46397  stoweidlem27  46455  dirkeritg  46530  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem39  46574  fourierdlem57  46591  fourierdlem58  46592  fourierdlem60  46594  fourierdlem61  46595  fourierdlem73  46607  fourierdlem83  46617  subsaliuncllem  46785  0ome  46957  hoi2toco  47035  elbigofrcl  49026  itcoval0mpt  49142