Theorem dmmptg 6244

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 2769	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6242	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3484	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3108	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3456	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 237	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2823	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  ∀wral 3085  {crab 3423  Vcvv 3463   ↦ cmpt 5196  dom cdm 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-mpt 5197  df-xp 5668  df-rel 5669  df-cnv 5670  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675

This theorem is referenced by:  rnmpt0f  6245  ovmpt3rabdm  7670  suppssov1  8193  suppssov2  8194  suppssfv  8198  iinon  8327  onoviun  8330  noinfep  9629  cantnfdm  9633  axcc2lem  10420  negfi  12164  ccatalpha  14631  swrd0  14696  o1lo1  15588  o1lo12  15589  lo1mptrcl  15673  o1mptrcl  15674  o1add2  15675  o1mul2  15676  o1sub2  15677  lo1add  15678  lo1mul  15679  o1dif  15681  rlimneg  15698  lo1le  15703  rlimno1  15705  o1fsum  15865  divsfval  17601  subdrgint  20884  iscnp2  23365  ptcnplem  23747  xkoinjcn  23813  fbasrn  24010  prdsdsf  24493  ressprdsds  24497  mbfmptcl  25764  mbfdm2  25765  dvmptresicc  26044  dvmptcl  26087  dvmptadd  26088  dvmptmul  26089  dvmptres2  26090  dvmptcmul  26092  dvmptcj  26096  dvmptco  26100  rolle  26118  dvlip  26121  dvlipcn  26122  dvle  26135  dvivthlem1  26136  dvivth  26138  dvfsumle  26149  dvfsumge  26150  dvmptrecl  26152  dvfsumlem2  26155  pserdv  26558  logtayl  26791  relogbf  26922  rlimcxp  27104  o1cxp  27105  gsummpt2co  33309  psgnfzto1stlem  33361  measdivcstALTV  34560  probfinmeasbALTV  34764  probmeasb  34765  dstrvprob  34807  cvmsss2  35699  sdclem2  38315  3factsumint1  42712  dmmzp  43390  dvcosax  46566  dvnprodlem3  46588  itgcoscmulx  46609  stoweidlem27  46667  dirkeritg  46742  fourierdlem16  46763  fourierdlem21  46768  fourierdlem22  46769  fourierdlem39  46786  fourierdlem57  46803  fourierdlem58  46804  fourierdlem60  46806  fourierdlem61  46807  fourierdlem73  46819  fourierdlem83  46829  subsaliuncllem  46997  0ome  47169  hoi2toco  47247  elbigofrcl  49249  itcoval0mpt  49365