Theorem cusgredgex2

Description: Any two distinct vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 4-Oct-2023)

	Ref	Expression
Hypotheses	cusgredgex2.1	|- V = ( Vtx ` G )
	cusgredgex2.2	|- E = ( Edg ` G )
Assertion	cusgredgex2	|- ( G e. ComplUSGraph -> ( ( A e. V /\ B e. V /\ A =/= B ) -> { A , B } e. E ) )

Proof

Step	Hyp	Ref	Expression
1		cusgredgex2.1	|- V = ( Vtx ` G )
2		cusgredgex2.2	|- E = ( Edg ` G )
3		eldifsn	|- ( B e. ( V \ { A } ) <-> ( B e. V /\ B =/= A ) )
4		necom	|- ( B =/= A <-> A =/= B )
5	4	anbi2i	|- ( ( B e. V /\ B =/= A ) <-> ( B e. V /\ A =/= B ) )
6	3 5	sylbbr	|- ( ( B e. V /\ A =/= B ) -> B e. ( V \ { A } ) )
7	6	anim2i	|- ( ( A e. V /\ ( B e. V /\ A =/= B ) ) -> ( A e. V /\ B e. ( V \ { A } ) ) )
8	7	3impb	|- ( ( A e. V /\ B e. V /\ A =/= B ) -> ( A e. V /\ B e. ( V \ { A } ) ) )
9	1 2	cusgredgex	|- ( G e. ComplUSGraph -> ( ( A e. V /\ B e. ( V \ { A } ) ) -> { A , B } e. E ) )
10	8 9	syl5	|- ( G e. ComplUSGraph -> ( ( A e. V /\ B e. V /\ A =/= B ) -> { A , B } e. E ) )