# 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}=\mathrm{Vtx}\left({G}\right)$
frcond1.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion frcond2 ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\to \exists !{b}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)$

### Proof

Step Hyp Ref Expression
1 frcond1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 frcond1.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 1 2 frcond1 ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\to \exists !{b}\in {V}\phantom{\rule{.4em}{0ex}}\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right)$
4 prex ${⊢}\left\{{A},{b}\right\}\in \mathrm{V}$
5 prex ${⊢}\left\{{b},{C}\right\}\in \mathrm{V}$
6 4 5 prss ${⊢}\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)↔\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}$
7 6 bicomi ${⊢}\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}↔\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)$
8 7 reubii ${⊢}\exists !{b}\in {V}\phantom{\rule{.4em}{0ex}}\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}↔\exists !{b}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)$
9 3 8 syl6ib ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\to \exists !{b}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)$