Theorem dmmptss 5790

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 5789	. 2 ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		ssrab2 3826	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ⊆ 𝐴
4	2, 3	eqsstri 3774	1 ⊢ dom 𝐹 ⊆ 𝐴

Syntax hints:   = wceq 1630   ∈ wcel 2137  {crab 3052  Vcvv 3338   ⊆ wss 3713   ↦ cmpt 4879  dom cdm 5264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pr 5053

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-rab 3057  df-v 3340  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-br 4803  df-opab 4863  df-mpt 4880  df-xp 5270  df-rel 5271  df-cnv 5272  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277

This theorem is referenced by:  mptrcl  6449  fvmptss  6452  fvmptex  6454  fvmptnf  6462  elfvmptrab1  6465  mptexg  6646  dmmpt2ssx  7401  curry1val  7436  curry2val  7440  tposssxp  7523  mptfi  8428  cnvimamptfin  8430  cantnfres  8745  mptct  9550  bitsval  15346  subcrcl  16675  arwval  16892  arwrcl  16893  coafval  16913  submrcl  17545  issubg  17793  isnsg  17822  cntzrcl  17958  gsumconst  18532  abvrcl  19021  psrass1lem  19577  psrass1  19605  psrass23l  19608  psrcom  19609  psrass23  19610  mpfrcl  19718  psropprmul  19808  coe1mul2  19839  isobs  20264  lmrcl  21235  1stcrestlem  21455  islocfin  21520  kgeni  21540  ptbasfi  21584  isxms2  22452  setsmstopn  22482  tngtopn  22653  isphtpc  22992  pcofval  23008  cfili  23264  cfilfcls  23270  rrxmval  23386  plybss  24147  ulmss  24348  dchrrcl  25162  gsummpt2co  30087  locfinreflem  30214  sitgclg  30711  cvmsrcl  31551  snmlval  31618  eldiophb  37820  elmnc  38206  itgocn  38234  issdrg  38267  submgmrcl  42290  dmmpt2ssx2  42623