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

Metamath Proof Explorer

Theorem idrval

Description: The value of the identity element. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	idrval.1	$⊢ X = ran G$
	idrval.2	$⊢ U = GId (G)$
Assertion	idrval	$⊢ G \in A \to U = (ι u \in X \| \forall x \in X (u G x = x \land x G u = x))$

Proof

Step	Hyp	Ref	Expression
1		idrval.1	$⊢ X = ran G$
2		idrval.2	$⊢ U = GId (G)$
3	1	gidval	$⊢ G \in A \to GId (G) = (ι u \in X \| \forall x \in X (u G x = x \land x G u = x))$
4	2 3	eqtrid	$⊢ G \in A \to U = (ι u \in X \| \forall x \in X (u G x = x \land x G u = x))$