Metamath Proof Explorer

Theorem bj-elres

Description: Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011) (Proof shortened by Peter Mazsa, 9-Sep-2022) Use the x B y idiom. (Revised by BJ, 16-Oct-2026)

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

Proof

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		bj-elinxp	$⊢ A \in (B \cap (C \times V)) \leftrightarrow \exists x \in C \exists y \in V (A = ⟨x, y⟩ \land x B y)$
4		rexv	$⊢ \exists y \in V (A = ⟨x, y⟩ \land x B y) \leftrightarrow \exists y (A = ⟨x, y⟩ \land x B y)$
5	4	rexbii	$⊢ \exists x \in C \exists y \in V (A = ⟨x, y⟩ \land x B y) \leftrightarrow \exists x \in C \exists y (A = ⟨x, y⟩ \land x B y)$
6	2 3 5	3bitri	$⊢ A \in ({B ↾}_{C}) \leftrightarrow \exists x \in C \exists y (A = ⟨x, y⟩ \land x B y)$