Metamath Proof Explorer

Theorem iscusgr

Description: The property of being a complete simple graph. (Contributed by AV, 1-Nov-2020)

Ref Expression
Assertion iscusgr 
|- ( G e. ComplUSGraph <-> ( G e. USGraph /\ G e. ComplGraph ) )

Proof

Step Hyp Ref Expression
1 df-cusgr 
 |-  ComplUSGraph = ( USGraph i^i ComplGraph )
2 1 elin2 
 |-  ( G e. ComplUSGraph <-> ( G e. USGraph /\ G e. ComplGraph ) )