Description: If a class is a subgraph of another class, both classes are sets. (Contributed by AV, 16-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | subgrv | ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relsubgr | ⊢ Rel SubGraph | |
2 | 1 | brrelex12i | ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) ) |