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


Ref 
Expression 

Hypothesis 
uhgredgiedgb.i 
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) 

Assertion 
uhgredgiedgb 
⊢ ( 𝐺 ∈ UHGraph → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom 𝐼 𝐸 = ( 𝐼 ‘ 𝑥 ) ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

uhgredgiedgb.i 
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) 
2 
1

uhgrfun 
⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 ) 
3 
1

edgiedgb 
⊢ ( Fun 𝐼 → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom 𝐼 𝐸 = ( 𝐼 ‘ 𝑥 ) ) ) 
4 
2 3

syl 
⊢ ( 𝐺 ∈ UHGraph → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom 𝐼 𝐸 = ( 𝐼 ‘ 𝑥 ) ) ) 