Theorem dmmptss 6084

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 6083	. 2 ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3	2	ssrab3 3981	1 ⊢ dom 𝐹 ⊆ 𝐴

Syntax hints:   = wceq 1543   ∈ wcel 2112  Vcvv 3398   ⊆ wss 3853   ↦ cmpt 5120  dom cdm 5536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040  df-opab 5102  df-mpt 5121  df-xp 5542  df-rel 5543  df-cnv 5544  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549

This theorem is referenced by:  mptrcl  6805  fvmptss  6808  fvmptex  6810  fvmptnf  6818  elfvmptrab1w  6822  elfvmptrab1  6823  mptexg  7015  mptexw  7704  dmmpossx  7814  tposssxp  7950  mptfi  8953  cnvimamptfin  8955  cantnfres  9270  mptct  10117  arwrcl  17504  cntzrcl  18675  gsumconst  19273  psrass1lemOLD  20853  psrass1lem  20856  psrass1  20884  psrass23l  20887  psrcom  20888  psrass23  20889  mpfrcl  20999  psropprmul  21113  coe1mul2  21144  lmrcl  22082  1stcrestlem  22303  ptbasfi  22432  isxms2  23300  setsmstopn  23330  tngtopn  23502  rrxmval  24256  ulmss  25243  dchrrcl  26075  gsummpt2co  30981  locfinreflem  31458  sitgclg  31975  cvmsrcl  32893  snmlval  32960  gonan0  33021  bj-fvmptunsn1  35112  eldiophb  40223  elmnc  40605  itgocn  40633  submgmrcl  44952  dmmpossx2  45288