Metamath Proof Explorer


Theorem dmsnopss

Description: The domain of a singleton of an ordered pair is a subset of the singleton of the first member (with no sethood assumptions on B ). (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion dmsnopss dom A B A

Proof

Step Hyp Ref Expression
1 dmsnopg B V dom A B = A
2 eqimss dom A B = A dom A B A
3 1 2 syl B V dom A B A
4 opprc2 ¬ B V A B =
5 4 sneqd ¬ B V A B =
6 5 dmeqd ¬ B V dom A B = dom
7 dmsn0 dom =
8 6 7 eqtrdi ¬ B V dom A B =
9 0ss A
10 8 9 eqsstrdi ¬ B V dom A B A
11 3 10 pm2.61i dom A B A