elrelimasn

Description: Elementhood in the image of a singleton. (Contributed by Mario Carneiro, 3-Nov-2015)

		Ref	Expression
	Assertion	elrelimasn	$⊢ Rel R \to (B \in R [\{A\}] \leftrightarrow A R B)$

Step	Hyp	Ref	Expression
1		relimasn	$⊢ Rel R \to R [\{A\}] = \{x \| A R x\}$
2	1	eleq2d	$⊢ Rel R \to (B \in R [\{A\}] \leftrightarrow B \in \{x \| A R x\})$
3		brrelex2	$⊢ (Rel R \land A R B) \to B \in V$
4	3	ex	$⊢ Rel R \to (A R B \to B \in V)$
5		breq2	$⊢ x = B \to (A R x \leftrightarrow A R B)$
6	5	elab3g	$⊢ (A R B \to B \in V) \to (B \in \{x \| A R x\} \leftrightarrow A R B)$
7	4 6	syl	$⊢ Rel R \to (B \in \{x \| A R x\} \leftrightarrow A R B)$
8	2 7	bitrd	$⊢ Rel R \to (B \in R [\{A\}] \leftrightarrow A R B)$

Metamath Proof Explorer