Metamath Proof Explorer


Theorem dmmptssf

Description: The domain of a mapping is a subset of its base class. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses dmmptssf.1
|- F/_ x A
dmmptssf.2
|- F = ( x e. A |-> B )
Assertion dmmptssf
|- dom F C_ A

Proof

Step Hyp Ref Expression
1 dmmptssf.1
 |-  F/_ x A
2 dmmptssf.2
 |-  F = ( x e. A |-> B )
3 2 dmmpt
 |-  dom F = { x e. A | B e. _V }
4 1 ssrab2f
 |-  { x e. A | B e. _V } C_ A
5 3 4 eqsstri
 |-  dom F C_ A