Metamath Proof Explorer

Theorem iedgvalprc

Description: Degenerated case 4 for edges: The set of indexed edges of a proper class is the empty set. (Contributed by AV, 12-Oct-2020)

Ref Expression
Assertion iedgvalprc C V iEdg C =


Step Hyp Ref Expression
1 df-nel C V ¬ C V
2 fvprc ¬ C V iEdg C =
3 1 2 sylbi C V iEdg C =