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 = ( Vtx ` G )
	frcond1.e	|- E = ( Edg ` G )
Assertion	frcond2	|- ( G e. FriendGraph -> ( ( A e. V /\ C e. V /\ A =/= C ) -> E! b e. V ( { A , b } e. E /\ { b , C } e. E ) ) )

Proof

Step	Hyp	Ref	Expression
1		frcond1.v	|- V = ( Vtx ` G )
2		frcond1.e	|- E = ( Edg ` G )
3	1 2	frcond1	|- ( G e. FriendGraph -> ( ( A e. V /\ C e. V /\ A =/= C ) -> E! b e. V { { A , b } , { b , C } } C_ E ) )
4		prex	|- { A , b } e. _V
5		prex	|- { b , C } e. _V
6	4 5	prss	|- ( ( { A , b } e. E /\ { b , C } e. E ) <-> { { A , b } , { b , C } } C_ E )
7	6	bicomi	|- ( { { A , b } , { b , C } } C_ E <-> ( { A , b } e. E /\ { b , C } e. E ) )
8	7	reubii	|- ( E! b e. V { { A , b } , { b , C } } C_ E <-> E! b e. V ( { A , b } e. E /\ { b , C } e. E ) )
9	3 8	syl6ib	|- ( G e. FriendGraph -> ( ( A e. V /\ C e. V /\ A =/= C ) -> E! b e. V ( { A , b } e. E /\ { b , C } e. E ) ) )