Theorem dmmptg 6200

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 2736	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6198	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3461	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3073	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3432	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 234	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2790	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∀wral 3051  {crab 3399  Vcvv 3440   ↦ cmpt 5179  dom cdm 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-mpt 5180  df-xp 5630  df-rel 5631  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  rnmpt0f  6201  ovmpt3rabdm  7617  suppssov1  8139  suppssov2  8140  suppssfv  8144  iinon  8272  onoviun  8275  noinfep  9569  cantnfdm  9573  axcc2lem  10346  negfi  12091  ccatalpha  14517  swrd0  14582  o1lo1  15460  o1lo12  15461  lo1mptrcl  15545  o1mptrcl  15546  o1add2  15547  o1mul2  15548  o1sub2  15549  lo1add  15550  lo1mul  15551  o1dif  15553  rlimneg  15570  lo1le  15575  rlimno1  15577  o1fsum  15736  divsfval  17468  subdrgint  20736  iscnp2  23183  ptcnplem  23565  xkoinjcn  23631  fbasrn  23828  prdsdsf  24311  ressprdsds  24315  mbfmptcl  25593  mbfdm2  25594  dvmptresicc  25873  dvmptcl  25919  dvmptadd  25920  dvmptmul  25921  dvmptres2  25922  dvmptcmul  25924  dvmptcj  25928  dvmptco  25932  rolle  25950  dvlip  25954  dvlipcn  25955  dvle  25968  dvivthlem1  25969  dvivth  25971  dvfsumle  25982  dvfsumleOLD  25983  dvfsumge  25984  dvmptrecl  25986  dvfsumlem2  25989  dvfsumlem2OLD  25990  pserdv  26395  logtayl  26625  relogbf  26757  rlimcxp  26940  o1cxp  26941  gsummpt2co  33131  psgnfzto1stlem  33182  measdivcstALTV  34382  probfinmeasbALTV  34586  probmeasb  34587  dstrvprob  34629  cvmsss2  35468  sdclem2  37943  3factsumint1  42275  dmmzp  42975  dvcosax  46170  dvnprodlem3  46192  itgcoscmulx  46213  stoweidlem27  46271  dirkeritg  46346  fourierdlem16  46367  fourierdlem21  46372  fourierdlem22  46373  fourierdlem39  46390  fourierdlem57  46407  fourierdlem58  46408  fourierdlem60  46410  fourierdlem61  46411  fourierdlem73  46423  fourierdlem83  46433  subsaliuncllem  46601  0ome  46773  hoi2toco  46851  elbigofrcl  48796  itcoval0mpt  48912