Theorem dmmptg 5549

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 3185	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
2	1	ralimi 2936	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
3		rabid2 3096	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
4	2, 3	sylibr 223	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
5		eqid 2610	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
6	5	dmmpt 5547	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
7	4, 6	syl6reqr 2663	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  ∀wral 2896  {crab 2900  Vcvv 3173   ↦ cmpt 4643  dom cdm 5038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-mpt 4645  df-xp 5044  df-rel 5045  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051

This theorem is referenced by:  ovmpt3rabdm  6790  suppssov1  7214  suppssfv  7218  iinon  7324  onoviun  7327  noinfep  8440  cantnfdm  8444  axcc2lem  9141  negfi  10850  ccatalpha  13228  swrd0  13286  o1lo1  14116  o1lo12  14117  lo1mptrcl  14200  o1mptrcl  14201  o1add2  14202  o1mul2  14203  o1sub2  14204  lo1add  14205  lo1mul  14206  o1dif  14208  rlimneg  14225  lo1le  14230  rlimno1  14232  o1fsum  14386  divsfval  16030  iscnp2  20853  ptcnplem  21234  xkoinjcn  21300  fbasrn  21498  prdsdsf  21982  ressprdsds  21986  mbfmptcl  23210  mbfdm2  23211  dvmptcl  23528  dvmptadd  23529  dvmptmul  23530  dvmptres2  23531  dvmptcmul  23533  dvmptcj  23537  dvmptco  23541  rolle  23557  dvlip  23560  dvlipcn  23561  dvle  23574  dvivthlem1  23575  dvivth  23577  dvfsumle  23588  dvfsumge  23589  dvmptrecl  23591  dvfsumlem2  23594  pserdv  23987  logtayl  24206  relogbf  24329  rlimcxp  24500  o1cxp  24501  gsummpt2co  29111  psgnfzto1stlem  29181  measdivcstOLD  29614  probfinmeasbOLD  29817  probmeasb  29819  dstrvprob  29860  cvmsss2  30510  sdclem2  32708  dmmzp  36314  rnmpt0  38407  dvmptresicc  38809  dvcosax  38816  dvnprodlem3  38838  itgcoscmulx  38861  stoweidlem27  38920  dirkeritg  38995  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem39  39039  fourierdlem57  39056  fourierdlem58  39057  fourierdlem60  39059  fourierdlem61  39060  fourierdlem73  39072  fourierdlem83  39082  subsaliuncllem  39251  0ome  39419  hoi2toco  39497  elbigofrcl  42142