elsnres

Description: Membership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011)

		Ref	Expression
	Hypothesis	elsnres.1	$⊢ C \in V$
	Assertion	elsnres	$⊢ A \in ({B ↾}_{\{C\}}) \leftrightarrow \exists y (A = ⟨C, y⟩ \land ⟨C, y⟩ \in B)$

Step	Hyp	Ref	Expression
1		elsnres.1	$⊢ C \in V$
2		elres	$⊢ A \in ({B ↾}_{\{C\}}) \leftrightarrow \exists x \in \{C\} \exists y (A = ⟨x, y⟩ \land ⟨x, y⟩ \in B)$
3		rexcom4	$⊢ \exists x \in \{C\} \exists y (A = ⟨x, y⟩ \land ⟨x, y⟩ \in B) \leftrightarrow \exists y \exists x \in \{C\} (A = ⟨x, y⟩ \land ⟨x, y⟩ \in B)$
4		opeq1	$⊢ x = C \to ⟨x, y⟩ = ⟨C, y⟩$
5	4	eqeq2d	$⊢ x = C \to (A = ⟨x, y⟩ \leftrightarrow A = ⟨C, y⟩)$
6	4	eleq1d	$⊢ x = C \to (⟨x, y⟩ \in B \leftrightarrow ⟨C, y⟩ \in B)$
7	5 6	anbi12d	$⊢ x = C \to ((A = ⟨x, y⟩ \land ⟨x, y⟩ \in B) \leftrightarrow (A = ⟨C, y⟩ \land ⟨C, y⟩ \in B))$
8	1 7	rexsn	$⊢ \exists x \in \{C\} (A = ⟨x, y⟩ \land ⟨x, y⟩ \in B) \leftrightarrow (A = ⟨C, y⟩ \land ⟨C, y⟩ \in B)$
9	8	exbii	$⊢ \exists y \exists x \in \{C\} (A = ⟨x, y⟩ \land ⟨x, y⟩ \in B) \leftrightarrow \exists y (A = ⟨C, y⟩ \land ⟨C, y⟩ \in B)$
10	2 3 9	3bitri	$⊢ A \in ({B ↾}_{\{C\}}) \leftrightarrow \exists y (A = ⟨C, y⟩ \land ⟨C, y⟩ \in B)$

Metamath Proof Explorer