Metamath Proof Explorer


Theorem opiedgfvi

Description: The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 4-Mar-2021)

Ref Expression
Hypotheses opvtxfvi.v
|- V e. _V
opvtxfvi.e
|- E e. _V
Assertion opiedgfvi
|- ( iEdg ` <. V , E >. ) = E

Proof

Step Hyp Ref Expression
1 opvtxfvi.v
 |-  V e. _V
2 opvtxfvi.e
 |-  E e. _V
3 opiedgfv
 |-  ( ( V e. _V /\ E e. _V ) -> ( iEdg ` <. V , E >. ) = E )
4 1 2 3 mp2an
 |-  ( iEdg ` <. V , E >. ) = E