This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funiedgdm2val

Description: The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020) (Revised by AV, 7-Jun-2021) (Revised by AV, 12-Nov-2021)

		Ref	Expression
	Hypotheses	funvtxdm2val.a	$⊢ A \in V$
		funvtxdm2val.b	$⊢ B \in V$
	Assertion	funiedgdm2val	$⊢ (Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \to iEdg (G) = ef (G)$

Proof

Step	Hyp	Ref	Expression
1		funvtxdm2val.a	$⊢ A \in V$
2		funvtxdm2val.b	$⊢ B \in V$
3		iedgval	$⊢ iEdg (G) = if (G \in (V \times V), 2^{nd} (G), ef (G))$
4	1 2	fun2dmnop0	$⊢ (Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \to \neg G \in (V \times V)$
5	4	iffalsed	$⊢ (Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \to if (G \in (V \times V), 2^{nd} (G), ef (G)) = ef (G)$
6	3 5	eqtrid	$⊢ (Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \to iEdg (G) = ef (G)$