Theorem dmmptg 6236

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3052  {crab 3420  Vcvv 3464   ↦ cmpt 5206  dom cdm 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-mpt 5207  df-xp 5665  df-rel 5666  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672

This theorem is referenced by:  rnmpt0f  6237  ovmpt3rabdm  7671  suppssov1  8201  suppssov2  8202  suppssfv  8206  iinon  8359  onoviun  8362  noinfep  9679  cantnfdm  9683  axcc2lem  10455  negfi  12196  ccatalpha  14616  swrd0  14681  o1lo1  15558  o1lo12  15559  lo1mptrcl  15643  o1mptrcl  15644  o1add2  15645  o1mul2  15646  o1sub2  15647  lo1add  15648  lo1mul  15649  o1dif  15651  rlimneg  15668  lo1le  15673  rlimno1  15675  o1fsum  15834  divsfval  17566  subdrgint  20768  iscnp2  23182  ptcnplem  23564  xkoinjcn  23630  fbasrn  23827  prdsdsf  24311  ressprdsds  24315  mbfmptcl  25594  mbfdm2  25595  dvmptresicc  25874  dvmptcl  25920  dvmptadd  25921  dvmptmul  25922  dvmptres2  25923  dvmptcmul  25925  dvmptcj  25929  dvmptco  25933  rolle  25951  dvlip  25955  dvlipcn  25956  dvle  25969  dvivthlem1  25970  dvivth  25972  dvfsumle  25983  dvfsumleOLD  25984  dvfsumge  25985  dvmptrecl  25987  dvfsumlem2  25990  dvfsumlem2OLD  25991  pserdv  26396  logtayl  26626  relogbf  26758  rlimcxp  26941  o1cxp  26942  gsummpt2co  33047  psgnfzto1stlem  33116  measdivcstALTV  34261  probfinmeasbALTV  34466  probmeasb  34467  dstrvprob  34509  cvmsss2  35301  sdclem2  37771  3factsumint1  42039  dmmzp  42723  dvcosax  45922  dvnprodlem3  45944  itgcoscmulx  45965  stoweidlem27  46023  dirkeritg  46098  fourierdlem16  46119  fourierdlem21  46124  fourierdlem22  46125  fourierdlem39  46142  fourierdlem57  46159  fourierdlem58  46160  fourierdlem60  46162  fourierdlem61  46163  fourierdlem73  46175  fourierdlem83  46185  subsaliuncllem  46353  0ome  46525  hoi2toco  46603  elbigofrcl  48497  itcoval0mpt  48613