Metamath Proof Explorer

Theorem fndmexb

Description: The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024)

		Ref	Expression
	Assertion	fndmexb	$⊢ F Fn A \to (A \in V \leftrightarrow F \in V)$

Step	Hyp	Ref	Expression
1		fnex	$⊢ (F Fn A \land A \in V) \to F \in V$
2	1	ex	$⊢ F Fn A \to (A \in V \to F \in V)$
3		simpr	$⊢ (F Fn A \land F \in V) \to F \in V$
4		simpl	$⊢ (F Fn A \land F \in V) \to F Fn A$
5	3 4	fndmexd	$⊢ (F Fn A \land F \in V) \to A \in V$
6	5	ex	$⊢ F Fn A \to (F \in V \to A \in V)$
7	2 6	impbid	$⊢ F Fn A \to (A \in V \leftrightarrow F \in V)$