Description: In a hypergraph, a set is an edge iff it is an indexed edge. (Contributed by AV, 17Oct2020)
Ref  Expression  

Hypothesis  uhgredgiedgb.i   I = ( iEdg ` G ) 

Assertion  uhgredgiedgb   ( G e. UHGraph > ( E e. ( Edg ` G ) <> E. x e. dom I E = ( I ` x ) ) ) 
Step  Hyp  Ref  Expression 

1  uhgredgiedgb.i   I = ( iEdg ` G ) 

2  1  uhgrfun   ( G e. UHGraph > Fun I ) 
3  1  edgiedgb   ( Fun I > ( E e. ( Edg ` G ) <> E. x e. dom I E = ( I ` x ) ) ) 
4  2 3  syl   ( G e. UHGraph > ( E e. ( Edg ` G ) <> E. x e. dom I E = ( I ` x ) ) ) 