elres

Description: Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011) (Proof shortened by Peter Mazsa, 9-Sep-2022)

		Ref	Expression
	Assertion	elres	$⊢ A \in ({B ↾}_{C}) \leftrightarrow \exists x \in C \exists y (A = ⟨x, y⟩ \land ⟨x, y⟩ \in B)$

Step	Hyp	Ref	Expression
1		df-res	$⊢ {B ↾}_{C} = B \cap (C \times V)$
2	1	eleq2i	$⊢ A \in ({B ↾}_{C}) \leftrightarrow A \in (B \cap (C \times V))$
3		elinxp	$⊢ A \in (B \cap (C \times V)) \leftrightarrow \exists x \in C \exists y \in V (A = ⟨x, y⟩ \land ⟨x, y⟩ \in B)$
4		rexv	$⊢ \exists y \in V (A = ⟨x, y⟩ \land ⟨x, y⟩ \in B) \leftrightarrow \exists y (A = ⟨x, y⟩ \land ⟨x, y⟩ \in B)$
5	4	rexbii	$⊢ \exists x \in C \exists y \in V (A = ⟨x, y⟩ \land ⟨x, y⟩ \in B) \leftrightarrow \exists x \in C \exists y (A = ⟨x, y⟩ \land ⟨x, y⟩ \in B)$
6	2 3 5	3bitri	$⊢ A \in ({B ↾}_{C}) \leftrightarrow \exists x \in C \exists y (A = ⟨x, y⟩ \land ⟨x, y⟩ \in B)$

Metamath Proof Explorer