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 e/ _V -> ( iEdg ` C ) = (/) )

Proof

Step Hyp Ref Expression
1 df-nel 
 |-  ( C e/ _V <-> -. C e. _V )
2 fvprc 
 |-  ( -. C e. _V -> ( iEdg ` C ) = (/) )
3 1 2 sylbi 
 |-  ( C e/ _V -> ( iEdg ` C ) = (/) )