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 -> ( A e. _V <-> F e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		fnex	|- ( ( F Fn A /\ A e. _V ) -> F e. _V )
2	1	ex	|- ( F Fn A -> ( A e. _V -> F e. _V ) )
3		simpr	|- ( ( F Fn A /\ F e. _V ) -> F e. _V )
4		simpl	|- ( ( F Fn A /\ F e. _V ) -> F Fn A )
5	3 4	fndmexd	|- ( ( F Fn A /\ F e. _V ) -> A e. _V )
6	5	ex	|- ( F Fn A -> ( F e. _V -> A e. _V ) )
7	2 6	impbid	|- ( F Fn A -> ( A e. _V <-> F e. _V ) )