Theorem dmmptg 6244

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 2769	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6242	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3484	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3108	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3456	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 237	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2823	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  ∀wral 3085  {crab 3423  Vcvv 3463   ↦ cmpt 5196  dom cdm 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-mpt 5197  df-xp 5668  df-rel 5669  df-cnv 5670  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675

This theorem is referenced by:  rnmpt0f  6245  ovmpt3rabdm  7670  suppssov1  8192  suppssov2  8193  suppssfv  8197  iinon  8326  onoviun  8329  noinfep  9628  cantnfdm  9632  axcc2lem  10419  negfi  12163  ccatalpha  14630  swrd0  14695  o1lo1  15587  o1lo12  15588  lo1mptrcl  15672  o1mptrcl  15673  o1add2  15674  o1mul2  15675  o1sub2  15676  lo1add  15677  lo1mul  15678  o1dif  15680  rlimneg  15697  lo1le  15702  rlimno1  15704  o1fsum  15864  divsfval  17600  subdrgint  20883  iscnp2  23364  ptcnplem  23746  xkoinjcn  23812  fbasrn  24009  prdsdsf  24492  ressprdsds  24496  mbfmptcl  25763  mbfdm2  25764  dvmptresicc  26043  dvmptcl  26086  dvmptadd  26087  dvmptmul  26088  dvmptres2  26089  dvmptcmul  26091  dvmptcj  26095  dvmptco  26099  rolle  26117  dvlip  26120  dvlipcn  26121  dvle  26134  dvivthlem1  26135  dvivth  26137  dvfsumle  26148  dvfsumge  26149  dvmptrecl  26151  dvfsumlem2  26154  pserdv  26557  logtayl  26790  relogbf  26921  rlimcxp  27103  o1cxp  27104  gsummpt2co  33308  psgnfzto1stlem  33360  measdivcstALTV  34559  probfinmeasbALTV  34763  probmeasb  34764  dstrvprob  34806  cvmsss2  35664  sdclem2  38280  3factsumint1  42677  dmmzp  43355  dvcosax  46531  dvnprodlem3  46553  itgcoscmulx  46574  stoweidlem27  46632  dirkeritg  46707  fourierdlem16  46728  fourierdlem21  46733  fourierdlem22  46734  fourierdlem39  46751  fourierdlem57  46768  fourierdlem58  46769  fourierdlem60  46771  fourierdlem61  46772  fourierdlem73  46784  fourierdlem83  46794  subsaliuncllem  46962  0ome  47134  hoi2toco  47212  elbigofrcl  49214  itcoval0mpt  49330