funfvbrb

Description: Two ways to say that A is in the domain of F . (Contributed by Mario Carneiro, 1-May-2014)

		Ref	Expression
	Assertion	funfvbrb	$⊢ Fun F \to (A \in dom F \leftrightarrow A F F (A))$

Step	Hyp	Ref	Expression
1		funfvop	$⊢ (Fun F \land A \in dom F) \to ⟨A, F (A)⟩ \in F$
2		df-br	$⊢ A F F (A) \leftrightarrow ⟨A, F (A)⟩ \in F$
3	1 2	sylibr	$⊢ (Fun F \land A \in dom F) \to A F F (A)$
4		funrel	$⊢ Fun F \to Rel F$
5		releldm	$⊢ (Rel F \land A F F (A)) \to A \in dom F$
6	4 5	sylan	$⊢ (Fun F \land A F F (A)) \to A \in dom F$
7	3 6	impbida	$⊢ Fun F \to (A \in dom F \leftrightarrow A F F (A))$

Metamath Proof Explorer