Metamath Proof Explorer

Theorem subgrv

Description: If a class is a subgraph of another class, both classes are sets. (Contributed by AV, 16-Nov-2020)

Ref Expression
Assertion subgrv 
|- ( S SubGraph G -> ( S e. _V /\ G e. _V ) )

Proof

Step Hyp Ref Expression
1 relsubgr 
 |-  Rel SubGraph
2 1 brrelex12i 
 |-  ( S SubGraph G -> ( S e. _V /\ G e. _V ) )