Theorem dmmptg 6142

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 6140	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3448	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3088	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3312	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 233	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2798	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  ∀wral 3065  {crab 3069  Vcvv 3430   ↦ cmpt 5161  dom cdm 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-mpt 5162  df-xp 5594  df-rel 5595  df-cnv 5596  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601

This theorem is referenced by:  rnmpt0f  6143  ovmpt3rabdm  7519  suppssov1  7998  suppssfv  8002  iinon  8155  onoviun  8158  noinfep  9379  cantnfdm  9383  axcc2lem  10176  negfi  11907  ccatalpha  14279  swrd0  14352  o1lo1  15227  o1lo12  15228  lo1mptrcl  15312  o1mptrcl  15313  o1add2  15314  o1mul2  15315  o1sub2  15316  lo1add  15317  lo1mul  15318  o1dif  15320  rlimneg  15339  lo1le  15344  rlimno1  15346  o1fsum  15506  divsfval  17239  subdrgint  20052  iscnp2  22371  ptcnplem  22753  xkoinjcn  22819  fbasrn  23016  prdsdsf  23501  ressprdsds  23505  mbfmptcl  24781  mbfdm2  24782  dvmptresicc  25061  dvmptcl  25104  dvmptadd  25105  dvmptmul  25106  dvmptres2  25107  dvmptcmul  25109  dvmptcj  25113  dvmptco  25117  rolle  25135  dvlip  25138  dvlipcn  25139  dvle  25152  dvivthlem1  25153  dvivth  25155  dvfsumle  25166  dvfsumge  25167  dvmptrecl  25169  dvfsumlem2  25172  pserdv  25569  logtayl  25796  relogbf  25922  rlimcxp  26104  o1cxp  26105  gsummpt2co  31287  psgnfzto1stlem  31346  measdivcstALTV  32172  probfinmeasbALTV  32375  probmeasb  32376  dstrvprob  32417  cvmsss2  33215  sdclem2  35879  3factsumint1  40009  dmmzp  40535  dvcosax  43421  dvnprodlem3  43443  itgcoscmulx  43464  stoweidlem27  43522  dirkeritg  43597  fourierdlem16  43618  fourierdlem21  43623  fourierdlem22  43624  fourierdlem39  43641  fourierdlem57  43658  fourierdlem58  43659  fourierdlem60  43661  fourierdlem61  43662  fourierdlem73  43674  fourierdlem83  43684  subsaliuncllem  43850  0ome  44021  hoi2toco  44099  elbigofrcl  45848  itcoval0mpt  45964