dmmptss - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dmmptss		Structured version Visualization version GIF version

Theorem dmmptss 6248

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

Colors of variables: wff setvar class

Syntax hints: = wceq 1533 ∈ wcel 2098 Vcvv 3471 ⊆ wss 3947 ↦ cmpt 5233 dom cdm 5680

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2698 ax-sep 5301 ax-nul 5308 ax-pr 5431

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5151 df-opab 5213 df-mpt 5234 df-xp 5686 df-rel 5687 df-cnv 5688 df-dm 5690 df-rn 5691 df-res 5692 df-ima 5693

This theorem is referenced by: mptrcl 7017 fvmptss 7020 fvmptex 7022 fvmptnf 7030 elfvmptrab1w 7035 elfvmptrab1 7036 mptexg 7237 mptexw 7960 dmmpossx 8074 tposssxp 8240 mptfi 9381 cnvimamptfin 9383 cantnfres 9706 mptct 10567 arwrcl 18038 submgmrcl 18660 cntzrcl 19283 gsumconst 19894 psrass1lemOLD 21879 psrass1lem 21882 psrass1 21912 psrass23l 21915 psrcom 21916 psrass23 21917 mpfrcl 22036 psropprmul 22161 coe1mul2 22193 lmrcl 23153 1stcrestlem 23374 ptbasfi 23503 isxms2 24372 setsmstopn 24404 tngtopn 24585 rrxmval 25351 ulmss 26351 dchrrcl 27191 gsummpt2co 32780 locfinreflem 33446 sitgclg 33967 cvmsrcl 34879 snmlval 34946 gonan0 35007 bj-fvmptunsn1 36741 eldiophb 42180 elmnc 42563 itgocn 42591 dmmpossx2 47451

	
		OSZAR »