Theorem dmmptss 6190

Description: The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.)

Hypothesis

Ref	Expression
dmmpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
dmmptss	⊢ dom 𝐹 ⊆ 𝐴

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem dmmptss

Step	Hyp	Ref	Expression
1		dmmpt.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6189	. 2 ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3	2	ssrab3 4033	1 ⊢ dom 𝐹 ⊆ 𝐴

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3436   ⊆ wss 3903   ↦ cmpt 5173  dom cdm 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-mpt 5174  df-xp 5625  df-rel 5626  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632

This theorem is referenced by:  mptrcl  6939  fvmptss  6942  fvmptex  6944  fvmptnf  6952  elfvmptrab1w  6957  elfvmptrab1  6958  mptexg  7157  mptexw  7888  dmmpossx  8001  tposssxp  8163  mptfi  9241  cnvimamptfin  9243  cantnfres  9573  mptct  10432  arwrcl  17951  submgmrcl  18569  cntzrcl  19206  gsumconst  19813  psrass1lem  21839  psrass1  21871  psrass23l  21874  psrcom  21875  psrass23  21876  mpfrcl  21990  psropprmul  22120  coe1mul2  22153  lmrcl  23116  1stcrestlem  23337  ptbasfi  23466  isxms2  24334  setsmstopn  24364  tngtopn  24536  rrxmval  25303  ulmss  26304  dchrrcl  27149  gsummpt2co  33001  locfinreflem  33807  sitgclg  34310  cvmsrcl  35237  snmlval  35304  gonan0  35365  bj-fvmptunsn1  37231  eldiophb  42730  elmnc  43109  itgocn  43137  tannpoly  46874  dmmpossx2  48321  dmtposss  48860