Theorem dmmptg 6241

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 2732	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6239	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3492	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3083	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3464	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 233	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2791	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∀wral 3061  {crab 3432  Vcvv 3474   ↦ cmpt 5231  dom cdm 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-mpt 5232  df-xp 5682  df-rel 5683  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689

This theorem is referenced by:  rnmpt0f  6242  ovmpt3rabdm  7667  suppssov1  8185  suppssfv  8189  iinon  8342  onoviun  8345  noinfep  9657  cantnfdm  9661  axcc2lem  10433  negfi  12167  ccatalpha  14547  swrd0  14612  o1lo1  15485  o1lo12  15486  lo1mptrcl  15570  o1mptrcl  15571  o1add2  15572  o1mul2  15573  o1sub2  15574  lo1add  15575  lo1mul  15576  o1dif  15578  rlimneg  15597  lo1le  15602  rlimno1  15604  o1fsum  15763  divsfval  17497  subdrgint  20562  iscnp2  22963  ptcnplem  23345  xkoinjcn  23411  fbasrn  23608  prdsdsf  24093  ressprdsds  24097  mbfmptcl  25377  mbfdm2  25378  dvmptresicc  25657  dvmptcl  25700  dvmptadd  25701  dvmptmul  25702  dvmptres2  25703  dvmptcmul  25705  dvmptcj  25709  dvmptco  25713  rolle  25731  dvlip  25734  dvlipcn  25735  dvle  25748  dvivthlem1  25749  dvivth  25751  dvfsumle  25762  dvfsumge  25763  dvmptrecl  25765  dvfsumlem2  25768  pserdv  26165  logtayl  26392  relogbf  26520  rlimcxp  26702  o1cxp  26703  gsummpt2co  32458  psgnfzto1stlem  32517  measdivcstALTV  33509  probfinmeasbALTV  33714  probmeasb  33715  dstrvprob  33756  cvmsss2  34551  gg-dvfsumle  35468  gg-dvfsumlem2  35469  sdclem2  36913  3factsumint1  41192  dmmzp  41773  dvcosax  44941  dvnprodlem3  44963  itgcoscmulx  44984  stoweidlem27  45042  dirkeritg  45117  fourierdlem16  45138  fourierdlem21  45143  fourierdlem22  45144  fourierdlem39  45161  fourierdlem57  45178  fourierdlem58  45179  fourierdlem60  45181  fourierdlem61  45182  fourierdlem73  45194  fourierdlem83  45204  subsaliuncllem  45372  0ome  45544  hoi2toco  45622  elbigofrcl  47324  itcoval0mpt  47440