Theorem bj-fvimacnv0

Description: Variant of fvimacnv where membership of A in the domain is not needed provided the containing class B does not contain the empty set. Note that this antecedent would not be needed with Definition df-afv . (Contributed by BJ, 7-Jan-2024)

	Ref	Expression
Assertion	bj-fvimacnv0	|- ( ( Fun F /\ -. (/) e. B ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( ( F ` A ) = (/) -> ( ( F ` A ) e. B <-> (/) e. B ) )
2	1	biimpcd	|- ( ( F ` A ) e. B -> ( ( F ` A ) = (/) -> (/) e. B ) )
3	2	con3rr3	|- ( -. (/) e. B -> ( ( F ` A ) e. B -> -. ( F ` A ) = (/) ) )
4	3	imp	|- ( ( -. (/) e. B /\ ( F ` A ) e. B ) -> -. ( F ` A ) = (/) )
5		ndmfv	|- ( -. A e. dom F -> ( F ` A ) = (/) )
6	4 5	nsyl2	|- ( ( -. (/) e. B /\ ( F ` A ) e. B ) -> A e. dom F )
7		simpr	|- ( ( -. (/) e. B /\ ( F ` A ) e. B ) -> ( F ` A ) e. B )
8		fvimacnv	|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )
9	8	biimpd	|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B -> A e. ( `' F " B ) ) )
10	9	ex	|- ( Fun F -> ( A e. dom F -> ( ( F ` A ) e. B -> A e. ( `' F " B ) ) ) )
11	10	com3l	|- ( A e. dom F -> ( ( F ` A ) e. B -> ( Fun F -> A e. ( `' F " B ) ) ) )
12	6 7 11	sylc	|- ( ( -. (/) e. B /\ ( F ` A ) e. B ) -> ( Fun F -> A e. ( `' F " B ) ) )
13	12	ex	|- ( -. (/) e. B -> ( ( F ` A ) e. B -> ( Fun F -> A e. ( `' F " B ) ) ) )
14	13	com3r	|- ( Fun F -> ( -. (/) e. B -> ( ( F ` A ) e. B -> A e. ( `' F " B ) ) ) )
15	14	imp	|- ( ( Fun F /\ -. (/) e. B ) -> ( ( F ` A ) e. B -> A e. ( `' F " B ) ) )
16		fvimacnvi	|- ( ( Fun F /\ A e. ( `' F " B ) ) -> ( F ` A ) e. B )
17	16	ex	|- ( Fun F -> ( A e. ( `' F " B ) -> ( F ` A ) e. B ) )
18	17	adantr	|- ( ( Fun F /\ -. (/) e. B ) -> ( A e. ( `' F " B ) -> ( F ` A ) e. B ) )
19	15 18	impbid	|- ( ( Fun F /\ -. (/) e. B ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )