Theorem dmmptg 6229

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 2762	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6227	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3475	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3099	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3447	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 236	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2816	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  ∀wral 3076  {crab 3414  Vcvv 3454   ↦ cmpt 5181  dom cdm 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3077  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-xp 5653  df-rel 5654  df-cnv 5655  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660

This theorem is referenced by:  rnmpt0f  6230  ovmpt3rabdm  7655  suppssov1  8177  suppssov2  8178  suppssfv  8182  iinon  8311  onoviun  8314  noinfep  9615  cantnfdm  9619  axcc2lem  10393  negfi  12141  ccatalpha  14607  swrd0  14672  o1lo1  15564  o1lo12  15565  lo1mptrcl  15649  o1mptrcl  15650  o1add2  15651  o1mul2  15652  o1sub2  15653  lo1add  15654  lo1mul  15655  o1dif  15657  rlimneg  15674  lo1le  15679  rlimno1  15681  o1fsum  15841  divsfval  17577  subdrgint  20849  iscnp2  23296  ptcnplem  23678  xkoinjcn  23744  fbasrn  23941  prdsdsf  24424  ressprdsds  24428  mbfmptcl  25695  mbfdm2  25696  dvmptresicc  25975  dvmptcl  26018  dvmptadd  26019  dvmptmul  26020  dvmptres2  26021  dvmptcmul  26023  dvmptcj  26027  dvmptco  26031  rolle  26049  dvlip  26052  dvlipcn  26053  dvle  26066  dvivthlem1  26067  dvivth  26069  dvfsumle  26080  dvfsumge  26081  dvmptrecl  26083  dvfsumlem2  26086  pserdv  26489  logtayl  26722  relogbf  26853  rlimcxp  27035  o1cxp  27036  gsummpt2co  33225  psgnfzto1stlem  33277  measdivcstALTV  34519  probfinmeasbALTV  34723  probmeasb  34724  dstrvprob  34766  cvmsss2  35621  sdclem2  38238  3factsumint1  42635  dmmzp  43311  dvcosax  46497  dvnprodlem3  46519  itgcoscmulx  46540  stoweidlem27  46598  dirkeritg  46673  fourierdlem16  46694  fourierdlem21  46699  fourierdlem22  46700  fourierdlem39  46717  fourierdlem57  46734  fourierdlem58  46735  fourierdlem60  46737  fourierdlem61  46738  fourierdlem73  46750  fourierdlem83  46760  subsaliuncllem  46928  0ome  47100  hoi2toco  47178  elbigofrcl  49169  itcoval0mpt  49285