Theorem dmmptg 6063

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 2798	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6061	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3459	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3128	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3334	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 237	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2852	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  ∀wral 3106  {crab 3110  Vcvv 3441   ↦ cmpt 5110  dom cdm 5519

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-mpt 5111  df-xp 5525  df-rel 5526  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532

This theorem is referenced by:  ovmpt3rabdm  7384  suppssov1  7845  suppssfv  7849  iinon  7960  onoviun  7963  noinfep  9107  cantnfdm  9111  axcc2lem  9847  negfi  11577  ccatalpha  13938  swrd0  14011  o1lo1  14886  o1lo12  14887  lo1mptrcl  14970  o1mptrcl  14971  o1add2  14972  o1mul2  14973  o1sub2  14974  lo1add  14975  lo1mul  14976  o1dif  14978  rlimneg  14995  lo1le  15000  rlimno1  15002  o1fsum  15160  divsfval  16812  subdrgint  19575  iscnp2  21844  ptcnplem  22226  xkoinjcn  22292  fbasrn  22489  prdsdsf  22974  ressprdsds  22978  mbfmptcl  24240  mbfdm2  24241  dvmptresicc  24519  dvmptcl  24562  dvmptadd  24563  dvmptmul  24564  dvmptres2  24565  dvmptcmul  24567  dvmptcj  24571  dvmptco  24575  rolle  24593  dvlip  24596  dvlipcn  24597  dvle  24610  dvivthlem1  24611  dvivth  24613  dvfsumle  24624  dvfsumge  24625  dvmptrecl  24627  dvfsumlem2  24630  pserdv  25024  logtayl  25251  relogbf  25377  rlimcxp  25559  o1cxp  25560  gsummpt2co  30733  psgnfzto1stlem  30792  measdivcstALTV  31594  probfinmeasbALTV  31797  probmeasb  31798  dstrvprob  31839  cvmsss2  32634  sdclem2  35180  3factsumint1  39309  dmmzp  39674  rnmpt0  41849  dvcosax  42568  dvnprodlem3  42590  itgcoscmulx  42611  stoweidlem27  42669  dirkeritg  42744  fourierdlem16  42765  fourierdlem21  42770  fourierdlem22  42771  fourierdlem39  42788  fourierdlem57  42805  fourierdlem58  42806  fourierdlem60  42808  fourierdlem61  42809  fourierdlem73  42821  fourierdlem83  42831  subsaliuncllem  42997  0ome  43168  hoi2toco  43246  elbigofrcl  44964  itcoval0mpt  45080