Theorem dmmptg 6191

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 2729	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6189	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3457	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3066	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3428	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 234	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2783	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3044  {crab 3394  Vcvv 3436   ↦ cmpt 5173  dom cdm 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-mpt 5174  df-xp 5625  df-rel 5626  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632

This theorem is referenced by:  rnmpt0f  6192  ovmpt3rabdm  7608  suppssov1  8130  suppssov2  8131  suppssfv  8135  iinon  8263  onoviun  8266  noinfep  9556  cantnfdm  9560  axcc2lem  10330  negfi  12074  ccatalpha  14500  swrd0  14565  o1lo1  15444  o1lo12  15445  lo1mptrcl  15529  o1mptrcl  15530  o1add2  15531  o1mul2  15532  o1sub2  15533  lo1add  15534  lo1mul  15535  o1dif  15537  rlimneg  15554  lo1le  15559  rlimno1  15561  o1fsum  15720  divsfval  17451  subdrgint  20688  iscnp2  23124  ptcnplem  23506  xkoinjcn  23572  fbasrn  23769  prdsdsf  24253  ressprdsds  24257  mbfmptcl  25535  mbfdm2  25536  dvmptresicc  25815  dvmptcl  25861  dvmptadd  25862  dvmptmul  25863  dvmptres2  25864  dvmptcmul  25866  dvmptcj  25870  dvmptco  25874  rolle  25892  dvlip  25896  dvlipcn  25897  dvle  25910  dvivthlem1  25911  dvivth  25913  dvfsumle  25924  dvfsumleOLD  25925  dvfsumge  25926  dvmptrecl  25928  dvfsumlem2  25931  dvfsumlem2OLD  25932  pserdv  26337  logtayl  26567  relogbf  26699  rlimcxp  26882  o1cxp  26883  gsummpt2co  33001  psgnfzto1stlem  33042  measdivcstALTV  34192  probfinmeasbALTV  34397  probmeasb  34398  dstrvprob  34440  cvmsss2  35251  sdclem2  37726  3factsumint1  41998  dmmzp  42710  dvcosax  45911  dvnprodlem3  45933  itgcoscmulx  45954  stoweidlem27  46012  dirkeritg  46087  fourierdlem16  46108  fourierdlem21  46113  fourierdlem22  46114  fourierdlem39  46131  fourierdlem57  46148  fourierdlem58  46149  fourierdlem60  46151  fourierdlem61  46152  fourierdlem73  46164  fourierdlem83  46174  subsaliuncllem  46342  0ome  46514  hoi2toco  46592  elbigofrcl  48539  itcoval0mpt  48655