Theorem dmmptg 6215

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 2729	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6213	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3468	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3066	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3439	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 234	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2783	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3044  {crab 3405  Vcvv 3447   ↦ cmpt 5188  dom cdm 5638

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-mpt 5189  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  6216  ovmpt3rabdm  7648  suppssov1  8176  suppssov2  8177  suppssfv  8181  iinon  8309  onoviun  8312  noinfep  9613  cantnfdm  9617  axcc2lem  10389  negfi  12132  ccatalpha  14558  swrd0  14623  o1lo1  15503  o1lo12  15504  lo1mptrcl  15588  o1mptrcl  15589  o1add2  15590  o1mul2  15591  o1sub2  15592  lo1add  15593  lo1mul  15594  o1dif  15596  rlimneg  15613  lo1le  15618  rlimno1  15620  o1fsum  15779  divsfval  17510  subdrgint  20712  iscnp2  23126  ptcnplem  23508  xkoinjcn  23574  fbasrn  23771  prdsdsf  24255  ressprdsds  24259  mbfmptcl  25537  mbfdm2  25538  dvmptresicc  25817  dvmptcl  25863  dvmptadd  25864  dvmptmul  25865  dvmptres2  25866  dvmptcmul  25868  dvmptcj  25872  dvmptco  25876  rolle  25894  dvlip  25898  dvlipcn  25899  dvle  25912  dvivthlem1  25913  dvivth  25915  dvfsumle  25926  dvfsumleOLD  25927  dvfsumge  25928  dvmptrecl  25930  dvfsumlem2  25933  dvfsumlem2OLD  25934  pserdv  26339  logtayl  26569  relogbf  26701  rlimcxp  26884  o1cxp  26885  gsummpt2co  32988  psgnfzto1stlem  33057  measdivcstALTV  34215  probfinmeasbALTV  34420  probmeasb  34421  dstrvprob  34463  cvmsss2  35261  sdclem2  37736  3factsumint1  42009  dmmzp  42721  dvcosax  45924  dvnprodlem3  45946  itgcoscmulx  45967  stoweidlem27  46025  dirkeritg  46100  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem39  46144  fourierdlem57  46161  fourierdlem58  46162  fourierdlem60  46164  fourierdlem61  46165  fourierdlem73  46177  fourierdlem83  46187  subsaliuncllem  46355  0ome  46527  hoi2toco  46605  elbigofrcl  48536  itcoval0mpt  48652