Theorem dmmptg 6261

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  ∀wral 3060  {crab 3435  Vcvv 3479   ↦ cmpt 5224  dom cdm 5684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-mpt 5225  df-xp 5690  df-rel 5691  df-cnv 5692  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697

This theorem is referenced by:  rnmpt0f  6262  ovmpt3rabdm  7693  suppssov1  8223  suppssov2  8224  suppssfv  8228  iinon  8381  onoviun  8384  noinfep  9701  cantnfdm  9705  axcc2lem  10477  negfi  12218  ccatalpha  14632  swrd0  14697  o1lo1  15574  o1lo12  15575  lo1mptrcl  15659  o1mptrcl  15660  o1add2  15661  o1mul2  15662  o1sub2  15663  lo1add  15664  lo1mul  15665  o1dif  15667  rlimneg  15684  lo1le  15689  rlimno1  15691  o1fsum  15850  divsfval  17593  subdrgint  20805  iscnp2  23248  ptcnplem  23630  xkoinjcn  23696  fbasrn  23893  prdsdsf  24378  ressprdsds  24382  mbfmptcl  25672  mbfdm2  25673  dvmptresicc  25952  dvmptcl  25998  dvmptadd  25999  dvmptmul  26000  dvmptres2  26001  dvmptcmul  26003  dvmptcj  26007  dvmptco  26011  rolle  26029  dvlip  26033  dvlipcn  26034  dvle  26047  dvivthlem1  26048  dvivth  26050  dvfsumle  26061  dvfsumleOLD  26062  dvfsumge  26063  dvmptrecl  26065  dvfsumlem2  26068  dvfsumlem2OLD  26069  pserdv  26474  logtayl  26703  relogbf  26835  rlimcxp  27018  o1cxp  27019  gsummpt2co  33052  psgnfzto1stlem  33121  measdivcstALTV  34227  probfinmeasbALTV  34432  probmeasb  34433  dstrvprob  34475  cvmsss2  35280  sdclem2  37750  3factsumint1  42023  dmmzp  42749  dvcosax  45946  dvnprodlem3  45968  itgcoscmulx  45989  stoweidlem27  46047  dirkeritg  46122  fourierdlem16  46143  fourierdlem21  46148  fourierdlem22  46149  fourierdlem39  46166  fourierdlem57  46183  fourierdlem58  46184  fourierdlem60  46186  fourierdlem61  46187  fourierdlem73  46199  fourierdlem83  46209  subsaliuncllem  46377  0ome  46549  hoi2toco  46627  elbigofrcl  48476  itcoval0mpt  48592