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	⊢ ( 𝐶 ∉ V → ( iEdg ‘ 𝐶 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-nel	⊢ ( 𝐶 ∉ V ↔ ¬ 𝐶 ∈ V )
2		fvprc	⊢ ( ¬ 𝐶 ∈ V → ( iEdg ‘ 𝐶 ) = ∅ )
3	1 2	sylbi	⊢ ( 𝐶 ∉ V → ( iEdg ‘ 𝐶 ) = ∅ )