Theorem dmmptg 6098

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		elex 3514	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
2	1	ralimi 3162	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
3		rabid2 3383	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
4	2, 3	sylibr 236	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
5		eqid 2823	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
6	5	dmmpt 6096	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
7	4, 6	syl6reqr 2877	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ∀wral 3140  {crab 3144  Vcvv 3496   ↦ cmpt 5148  dom cdm 5557

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-mpt 5149  df-xp 5563  df-rel 5564  df-cnv 5565  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570

This theorem is referenced by:  ovmpt3rabdm  7406  suppssov1  7864  suppssfv  7868  iinon  7979  onoviun  7982  noinfep  9125  cantnfdm  9129  axcc2lem  9860  negfi  11591  ccatalpha  13949  swrd0  14022  o1lo1  14896  o1lo12  14897  lo1mptrcl  14980  o1mptrcl  14981  o1add2  14982  o1mul2  14983  o1sub2  14984  lo1add  14985  lo1mul  14986  o1dif  14988  rlimneg  15005  lo1le  15010  rlimno1  15012  o1fsum  15170  divsfval  16822  subdrgint  19584  iscnp2  21849  ptcnplem  22231  xkoinjcn  22297  fbasrn  22494  prdsdsf  22979  ressprdsds  22983  mbfmptcl  24239  mbfdm2  24240  dvmptcl  24558  dvmptadd  24559  dvmptmul  24560  dvmptres2  24561  dvmptcmul  24563  dvmptcj  24567  dvmptco  24571  rolle  24589  dvlip  24592  dvlipcn  24593  dvle  24606  dvivthlem1  24607  dvivth  24609  dvfsumle  24620  dvfsumge  24621  dvmptrecl  24623  dvfsumlem2  24626  pserdv  25019  logtayl  25245  relogbf  25371  rlimcxp  25553  o1cxp  25554  gsummpt2co  30688  psgnfzto1stlem  30744  measdivcstALTV  31486  probfinmeasbALTV  31689  probmeasb  31690  dstrvprob  31731  cvmsss2  32523  sdclem2  35019  dmmzp  39337  rnmpt0  41490  dvmptresicc  42211  dvcosax  42218  dvnprodlem3  42240  itgcoscmulx  42261  stoweidlem27  42319  dirkeritg  42394  fourierdlem16  42415  fourierdlem21  42420  fourierdlem22  42421  fourierdlem39  42438  fourierdlem57  42455  fourierdlem58  42456  fourierdlem60  42458  fourierdlem61  42459  fourierdlem73  42471  fourierdlem83  42481  subsaliuncllem  42647  0ome  42818  hoi2toco  42896  elbigofrcl  44617