Theorem dmmptg 5632

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	|- ( A. x e. A B e. V -> dom ( x e. A |-> B ) = A )

Distinct variable group:   x, A

Allowed substitution hints:   B( x)   V( x)

Proof of Theorem dmmptg

Step	Hyp	Ref	Expression
1		elex 3212	. . . 4 |- ( B e. V -> B e. _V )
2	1	ralimi 2952	. . 3 |- ( A. x e. A B e. V -> A. x e. A B e. _V )
3		rabid2 3118	. . 3 |- ( A = { x e. A | B e. _V } <-> A. x e. A B e. _V )
4	2, 3	sylibr 224	. 2 |- ( A. x e. A B e. V -> A = { x e. A | B e. _V } )
5		eqid 2622	. . 3 |- ( x e. A |-> B ) = ( x e. A |-> B )
6	5	dmmpt 5630	. 2 |- dom ( x e. A |-> B ) = { x e. A | B e. _V }
7	4, 6	syl6reqr 2675	1 |- ( A. x e. A B e. V -> dom ( x e. A |-> B ) = A )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   A.wral 2912   {crab 2916   _Vcvv 3200   |-> cmpt 4729   dom cdm 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-mpt 4730  df-xp 5120  df-rel 5121  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127

This theorem is referenced by:  ovmpt3rabdm  6892  suppssov1  7327  suppssfv  7331  iinon  7437  onoviun  7440  noinfep  8557  cantnfdm  8561  axcc2lem  9258  negfi  10971  ccatalpha  13375  swrd0  13434  o1lo1  14268  o1lo12  14269  lo1mptrcl  14352  o1mptrcl  14353  o1add2  14354  o1mul2  14355  o1sub2  14356  lo1add  14357  lo1mul  14358  o1dif  14360  rlimneg  14377  lo1le  14382  rlimno1  14384  o1fsum  14545  divsfval  16207  iscnp2  21043  ptcnplem  21424  xkoinjcn  21490  fbasrn  21688  prdsdsf  22172  ressprdsds  22176  mbfmptcl  23404  mbfdm2  23405  dvmptcl  23722  dvmptadd  23723  dvmptmul  23724  dvmptres2  23725  dvmptcmul  23727  dvmptcj  23731  dvmptco  23735  rolle  23753  dvlip  23756  dvlipcn  23757  dvle  23770  dvivthlem1  23771  dvivth  23773  dvfsumle  23784  dvfsumge  23785  dvmptrecl  23787  dvfsumlem2  23790  pserdv  24183  logtayl  24406  relogbf  24529  rlimcxp  24700  o1cxp  24701  gsummpt2co  29780  psgnfzto1stlem  29850  measdivcstOLD  30287  probfinmeasbOLD  30490  probmeasb  30492  dstrvprob  30533  cvmsss2  31256  sdclem2  33538  dmmzp  37296  rnmpt0  39412  dvmptresicc  40134  dvcosax  40141  dvnprodlem3  40163  itgcoscmulx  40185  stoweidlem27  40244  dirkeritg  40319  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem39  40363  fourierdlem57  40380  fourierdlem58  40381  fourierdlem60  40383  fourierdlem61  40384  fourierdlem73  40396  fourierdlem83  40406  subsaliuncllem  40575  0ome  40743  hoi2toco  40821  elbigofrcl  42344