Theorem dmmptg 5851

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 3400	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
2	1	ralimi 3133	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
3		rabid2 3300	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
4	2, 3	sylibr 226	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
5		eqid 2799	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
6	5	dmmpt 5849	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
7	4, 6	syl6reqr 2852	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1653   ∈ wcel 2157  ∀wral 3089  {crab 3093  Vcvv 3385   ↦ cmpt 4922  dom cdm 5312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pr 5097

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-br 4844  df-opab 4906  df-mpt 4923  df-xp 5318  df-rel 5319  df-cnv 5320  df-dm 5322  df-rn 5323  df-res 5324  df-ima 5325

This theorem is referenced by:  ovmpt3rabdm  7126  suppssov1  7565  suppssfv  7569  iinon  7676  onoviun  7679  noinfep  8807  cantnfdm  8811  axcc2lem  9546  negfi  11263  ccatalpha  13613  swrd0  13687  o1lo1  14609  o1lo12  14610  lo1mptrcl  14693  o1mptrcl  14694  o1add2  14695  o1mul2  14696  o1sub2  14697  lo1add  14698  lo1mul  14699  o1dif  14701  rlimneg  14718  lo1le  14723  rlimno1  14725  o1fsum  14883  divsfval  16522  iscnp2  21372  ptcnplem  21753  xkoinjcn  21819  fbasrn  22016  prdsdsf  22500  ressprdsds  22504  mbfmptcl  23744  mbfdm2  23745  dvmptcl  24063  dvmptadd  24064  dvmptmul  24065  dvmptres2  24066  dvmptcmul  24068  dvmptcj  24072  dvmptco  24076  rolle  24094  dvlip  24097  dvlipcn  24098  dvle  24111  dvivthlem1  24112  dvivth  24114  dvfsumle  24125  dvfsumge  24126  dvmptrecl  24128  dvfsumlem2  24131  pserdv  24524  logtayl  24747  relogbf  24873  rlimcxp  25052  o1cxp  25053  gsummpt2co  30296  psgnfzto1stlem  30366  measdivcstOLD  30803  probfinmeasbOLD  31007  probmeasb  31009  dstrvprob  31050  cvmsss2  31773  sdclem2  34025  dmmzp  38082  rnmpt0  40164  dvmptresicc  40878  dvcosax  40885  dvnprodlem3  40907  itgcoscmulx  40928  stoweidlem27  40987  dirkeritg  41062  fourierdlem16  41083  fourierdlem21  41088  fourierdlem22  41089  fourierdlem39  41106  fourierdlem57  41123  fourierdlem58  41124  fourierdlem60  41126  fourierdlem61  41127  fourierdlem73  41139  fourierdlem83  41149  subsaliuncllem  41318  0ome  41489  hoi2toco  41567  elbigofrcl  43143