Theorem dmmptg 6144

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 2740	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6142	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3449	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3089	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3313	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 233	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2799	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2110  ∀wral 3066  {crab 3070  Vcvv 3431   ↦ cmpt 5162  dom cdm 5590

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-mpt 5163  df-xp 5596  df-rel 5597  df-cnv 5598  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603

This theorem is referenced by:  rnmpt0f  6145  ovmpt3rabdm  7522  suppssov1  8005  suppssfv  8009  iinon  8162  onoviun  8165  noinfep  9396  cantnfdm  9400  axcc2lem  10193  negfi  11924  ccatalpha  14296  swrd0  14369  o1lo1  15244  o1lo12  15245  lo1mptrcl  15329  o1mptrcl  15330  o1add2  15331  o1mul2  15332  o1sub2  15333  lo1add  15334  lo1mul  15335  o1dif  15337  rlimneg  15356  lo1le  15361  rlimno1  15363  o1fsum  15523  divsfval  17256  subdrgint  20069  iscnp2  22388  ptcnplem  22770  xkoinjcn  22836  fbasrn  23033  prdsdsf  23518  ressprdsds  23522  mbfmptcl  24798  mbfdm2  24799  dvmptresicc  25078  dvmptcl  25121  dvmptadd  25122  dvmptmul  25123  dvmptres2  25124  dvmptcmul  25126  dvmptcj  25130  dvmptco  25134  rolle  25152  dvlip  25155  dvlipcn  25156  dvle  25169  dvivthlem1  25170  dvivth  25172  dvfsumle  25183  dvfsumge  25184  dvmptrecl  25186  dvfsumlem2  25189  pserdv  25586  logtayl  25813  relogbf  25939  rlimcxp  26121  o1cxp  26122  gsummpt2co  31304  psgnfzto1stlem  31363  measdivcstALTV  32189  probfinmeasbALTV  32392  probmeasb  32393  dstrvprob  32434  cvmsss2  33232  sdclem2  35896  3factsumint1  40026  dmmzp  40552  dvcosax  43438  dvnprodlem3  43460  itgcoscmulx  43481  stoweidlem27  43539  dirkeritg  43614  fourierdlem16  43635  fourierdlem21  43640  fourierdlem22  43641  fourierdlem39  43658  fourierdlem57  43675  fourierdlem58  43676  fourierdlem60  43678  fourierdlem61  43679  fourierdlem73  43691  fourierdlem83  43701  subsaliuncllem  43867  0ome  44038  hoi2toco  44116  elbigofrcl  45865  itcoval0mpt  45981