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

Metamath Proof Explorer

Theorem elrid

Description: Characterization of the elements of a restricted identity relation. (Contributed by BJ, 28-Aug-2022) (Proof shortened by Peter Mazsa, 9-Sep-2022)

		Ref	Expression
	Assertion	elrid	$⊢ A \in ({I ↾}_{X}) \leftrightarrow \exists x \in X A = ⟨x, x⟩$

Proof

Step	Hyp	Ref	Expression
1		df-res	$⊢ {I ↾}_{X} = I \cap (X \times V)$
2	1	eleq2i	$⊢ A \in ({I ↾}_{X}) \leftrightarrow A \in (I \cap (X \times V))$
3		elidinxp	$⊢ A \in (I \cap (X \times V)) \leftrightarrow \exists x \in (X \cap V) A = ⟨x, x⟩$
4		inv1	$⊢ X \cap V = X$
5	4	rexeqi	$⊢ \exists x \in (X \cap V) A = ⟨x, x⟩ \leftrightarrow \exists x \in X A = ⟨x, x⟩$
6	2 3 5	3bitri	$⊢ A \in ({I ↾}_{X}) \leftrightarrow \exists x \in X A = ⟨x, x⟩$