Metamath Proof Explorer


Theorem funprg

Description: A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion funprg AVBWCXDYABFunACBD

Proof

Step Hyp Ref Expression
1 funsng AVCXFunAC
2 funsng BWDYFunBD
3 1 2 anim12i AVCXBWDYFunACFunBD
4 3 an4s AVBWCXDYFunACFunBD
5 4 3adant3 AVBWCXDYABFunACFunBD
6 dmsnopg CXdomAC=A
7 dmsnopg DYdomBD=B
8 6 7 ineqan12d CXDYdomACdomBD=AB
9 disjsn2 ABAB=
10 8 9 sylan9eq CXDYABdomACdomBD=
11 10 3adant1 AVBWCXDYABdomACdomBD=
12 funun FunACFunBDdomACdomBD=FunACBD
13 5 11 12 syl2anc AVBWCXDYABFunACBD
14 df-pr ACBD=ACBD
15 14 funeqi FunACBDFunACBD
16 13 15 sylibr AVBWCXDYABFunACBD