Metamath Proof Explorer


Theorem frcond2

Description: The friendship condition: any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Hypotheses frcond1.v V=VtxG
frcond1.e E=EdgG
Assertion frcond2 GFriendGraphAVCVAC∃!bVAbEbCE

Proof

Step Hyp Ref Expression
1 frcond1.v V=VtxG
2 frcond1.e E=EdgG
3 1 2 frcond1 GFriendGraphAVCVAC∃!bVAbbCE
4 prex AbV
5 prex bCV
6 4 5 prss AbEbCEAbbCE
7 6 bicomi AbbCEAbEbCE
8 7 reubii ∃!bVAbbCE∃!bVAbEbCE
9 3 8 syl6ib GFriendGraphAVCVAC∃!bVAbEbCE