Metamath Proof Explorer


Theorem funopdmsn

Description: The domain of a function which is an ordered pair is a singleton. (Contributed by AV, 15-Nov-2021) (Avoid depending on this detail.)

Ref Expression
Hypotheses funopdmsn.g G = X Y
funopdmsn.x X V
funopdmsn.y Y W
Assertion funopdmsn Fun G A dom G B dom G A = B

Proof

Step Hyp Ref Expression
1 funopdmsn.g G = X Y
2 funopdmsn.x X V
3 funopdmsn.y Y W
4 1 funeqi Fun G Fun X Y
5 2 elexi X V
6 3 elexi Y V
7 5 6 funop Fun X Y x X = x X Y = x x
8 4 7 bitri Fun G x X = x X Y = x x
9 1 eqcomi X Y = G
10 9 eqeq1i X Y = x x G = x x
11 dmeq G = x x dom G = dom x x
12 vex x V
13 12 dmsnop dom x x = x
14 11 13 eqtrdi G = x x dom G = x
15 eleq2 dom G = x A dom G A x
16 eleq2 dom G = x B dom G B x
17 15 16 anbi12d dom G = x A dom G B dom G A x B x
18 elsni A x A = x
19 elsni B x B = x
20 eqtr3 A = x B = x A = B
21 18 19 20 syl2an A x B x A = B
22 17 21 syl6bi dom G = x A dom G B dom G A = B
23 14 22 syl G = x x A dom G B dom G A = B
24 10 23 sylbi X Y = x x A dom G B dom G A = B
25 24 adantl X = x X Y = x x A dom G B dom G A = B
26 25 exlimiv x X = x X Y = x x A dom G B dom G A = B
27 8 26 sylbi Fun G A dom G B dom G A = B
28 27 3impib Fun G A dom G B dom G A = B