Metamath Proof Explorer


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=VtxG
cusgredgex2.2 E=EdgG
Assertion cusgredgex2 GComplUSGraphAVBVABABE

Proof

Step Hyp Ref Expression
1 cusgredgex2.1 V=VtxG
2 cusgredgex2.2 E=EdgG
3 eldifsn BVABVBA
4 necom BAAB
5 4 anbi2i BVBABVAB
6 3 5 sylbbr BVABBVA
7 6 anim2i AVBVABAVBVA
8 7 3impb AVBVABAVBVA
9 1 2 cusgredgex GComplUSGraphAVBVAABE
10 8 9 syl5 GComplUSGraphAVBVABABE