Metamath Proof Explorer


Theorem usgrprc

Description: The class of simple graphs is a proper class (and therefore, because of prcssprc , the classes of multigraphs, pseudographs and hypergraphs are proper classes, too). (Contributed by AV, 27-Dec-2020)

Ref Expression
Assertion usgrprc USGraphV

Proof

Step Hyp Ref Expression
1 eqid ve|e:=ve|e:
2 1 griedg0ssusgr ve|e:USGraph
3 1 griedg0prc ve|e:V
4 prcssprc ve|e:USGraphve|e:VUSGraphV
5 2 3 4 mp2an USGraphV