Theorem dmmptg 6199

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∀wral 3060  {crab 3405  Vcvv 3446   ↦ cmpt 5193  dom cdm 5638

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 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-mpt 5194  df-xp 5644  df-rel 5645  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by:  rnmpt0f  6200  ovmpt3rabdm  7617  suppssov1  8134  suppssfv  8138  iinon  8291  onoviun  8294  noinfep  9605  cantnfdm  9609  axcc2lem  10381  negfi  12113  ccatalpha  14493  swrd0  14558  o1lo1  15431  o1lo12  15432  lo1mptrcl  15516  o1mptrcl  15517  o1add2  15518  o1mul2  15519  o1sub2  15520  lo1add  15521  lo1mul  15522  o1dif  15524  rlimneg  15543  lo1le  15548  rlimno1  15550  o1fsum  15709  divsfval  17443  subdrgint  20326  iscnp2  22627  ptcnplem  23009  xkoinjcn  23075  fbasrn  23272  prdsdsf  23757  ressprdsds  23761  mbfmptcl  25037  mbfdm2  25038  dvmptresicc  25317  dvmptcl  25360  dvmptadd  25361  dvmptmul  25362  dvmptres2  25363  dvmptcmul  25365  dvmptcj  25369  dvmptco  25373  rolle  25391  dvlip  25394  dvlipcn  25395  dvle  25408  dvivthlem1  25409  dvivth  25411  dvfsumle  25422  dvfsumge  25423  dvmptrecl  25425  dvfsumlem2  25428  pserdv  25825  logtayl  26052  relogbf  26178  rlimcxp  26360  o1cxp  26361  gsummpt2co  31960  psgnfzto1stlem  32019  measdivcstALTV  32913  probfinmeasbALTV  33118  probmeasb  33119  dstrvprob  33160  cvmsss2  33955  sdclem2  36274  3factsumint1  40551  dmmzp  41114  dvcosax  44287  dvnprodlem3  44309  itgcoscmulx  44330  stoweidlem27  44388  dirkeritg  44463  fourierdlem16  44484  fourierdlem21  44489  fourierdlem22  44490  fourierdlem39  44507  fourierdlem57  44524  fourierdlem58  44525  fourierdlem60  44527  fourierdlem61  44528  fourierdlem73  44540  fourierdlem83  44550  subsaliuncllem  44718  0ome  44890  hoi2toco  44968  elbigofrcl  46756  itcoval0mpt  46872