Theorem dmmptg 6243

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 2763	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6241	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3476	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3102	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3449	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 237	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2817	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ∀wral 3079  {crab 3416  Vcvv 3455   ↦ cmpt 5192  dom cdm 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-mpt 5193  df-xp 5667  df-rel 5668  df-cnv 5669  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674

This theorem is referenced by:  rnmpt0f  6244  ovmpt3rabdm  7669  suppssov1  8189  suppssov2  8190  suppssfv  8194  iinon  8323  onoviun  8326  noinfep  9625  cantnfdm  9629  axcc2lem  10415  negfi  12159  ccatalpha  14627  swrd0  14692  o1lo1  15584  o1lo12  15585  lo1mptrcl  15669  o1mptrcl  15670  o1add2  15671  o1mul2  15672  o1sub2  15673  lo1add  15674  lo1mul  15675  o1dif  15677  rlimneg  15694  lo1le  15699  rlimno1  15701  o1fsum  15861  divsfval  17596  subdrgint  20906  iscnp2  23396  ptcnplem  23778  xkoinjcn  23844  fbasrn  24041  prdsdsf  24524  ressprdsds  24528  mbfmptcl  25795  mbfdm2  25796  dvmptresicc  26075  dvmptcl  26118  dvmptadd  26119  dvmptmul  26120  dvmptres2  26121  dvmptcmul  26123  dvmptcj  26127  dvmptco  26131  rolle  26149  dvlip  26152  dvlipcn  26153  dvle  26166  dvivthlem1  26167  dvivth  26169  dvfsumle  26180  dvfsumge  26181  dvmptrecl  26183  dvfsumlem2  26186  pserdv  26592  logtayl  26825  relogbf  26956  rlimcxp  27138  o1cxp  27139  gsummpt2co  33368  psgnfzto1stlem  33420  measdivcstALTV  34615  probfinmeasbALTV  34819  probmeasb  34820  dstrvprob  34862  cvmsss2  35766  sdclem2  38393  3factsumint1  42788  dmmzp  43464  dvcosax  46640  dvnprodlem3  46662  itgcoscmulx  46683  stoweidlem27  46741  dirkeritg  46816  fourierdlem16  46837  fourierdlem21  46842  fourierdlem22  46843  fourierdlem39  46860  fourierdlem57  46877  fourierdlem58  46878  fourierdlem60  46880  fourierdlem61  46881  fourierdlem73  46893  fourierdlem83  46903  subsaliuncllem  47071  0ome  47243  hoi2toco  47321  elbigofrcl  49330  itcoval0mpt  49446