Theorem dmmptg 6203

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 6201	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3465	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3066	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3436	. . 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 3402  Vcvv 3444   ↦ cmpt 5183  dom cdm 5631

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-mpt 5184  df-xp 5637  df-rel 5638  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  rnmpt0f  6204  ovmpt3rabdm  7628  suppssov1  8153  suppssov2  8154  suppssfv  8158  iinon  8286  onoviun  8289  noinfep  9589  cantnfdm  9593  axcc2lem  10365  negfi  12108  ccatalpha  14534  swrd0  14599  o1lo1  15479  o1lo12  15480  lo1mptrcl  15564  o1mptrcl  15565  o1add2  15566  o1mul2  15567  o1sub2  15568  lo1add  15569  lo1mul  15570  o1dif  15572  rlimneg  15589  lo1le  15594  rlimno1  15596  o1fsum  15755  divsfval  17486  subdrgint  20688  iscnp2  23102  ptcnplem  23484  xkoinjcn  23550  fbasrn  23747  prdsdsf  24231  ressprdsds  24235  mbfmptcl  25513  mbfdm2  25514  dvmptresicc  25793  dvmptcl  25839  dvmptadd  25840  dvmptmul  25841  dvmptres2  25842  dvmptcmul  25844  dvmptcj  25848  dvmptco  25852  rolle  25870  dvlip  25874  dvlipcn  25875  dvle  25888  dvivthlem1  25889  dvivth  25891  dvfsumle  25902  dvfsumleOLD  25903  dvfsumge  25904  dvmptrecl  25906  dvfsumlem2  25909  dvfsumlem2OLD  25910  pserdv  26315  logtayl  26545  relogbf  26677  rlimcxp  26860  o1cxp  26861  gsummpt2co  32961  psgnfzto1stlem  33030  measdivcstALTV  34188  probfinmeasbALTV  34393  probmeasb  34394  dstrvprob  34436  cvmsss2  35234  sdclem2  37709  3factsumint1  41982  dmmzp  42694  dvcosax  45897  dvnprodlem3  45919  itgcoscmulx  45940  stoweidlem27  45998  dirkeritg  46073  fourierdlem16  46094  fourierdlem21  46099  fourierdlem22  46100  fourierdlem39  46117  fourierdlem57  46134  fourierdlem58  46135  fourierdlem60  46137  fourierdlem61  46138  fourierdlem73  46150  fourierdlem83  46160  subsaliuncllem  46328  0ome  46500  hoi2toco  46578  elbigofrcl  48512  itcoval0mpt  48628