Theorem elmapintab

Description: Two ways to say a set is an element of mapped intersection of a class. Here F maps elements of C to elements of |^| { x | ph } or x . (Contributed by RP, 19-Aug-2020)

	Ref	Expression
Hypotheses	elmapintab.1	|- ( A e. B <-> ( A e. C /\ ( F ` A ) e. |^| { x | ph } ) )
	elmapintab.2	|- ( A e. E <-> ( A e. C /\ ( F ` A ) e. x ) )
Assertion	elmapintab	|- ( A e. B <-> ( A e. C /\ A. x ( ph -> A e. E ) ) )

Proof

Step	Hyp	Ref	Expression
1		elmapintab.1	|- ( A e. B <-> ( A e. C /\ ( F ` A ) e. |^| { x | ph } ) )
2		elmapintab.2	|- ( A e. E <-> ( A e. C /\ ( F ` A ) e. x ) )
3		fvex	|- ( F ` A ) e. _V
4	3	elintab	|- ( ( F ` A ) e. |^| { x | ph } <-> A. x ( ph -> ( F ` A ) e. x ) )
5	4	anbi2i	|- ( ( A e. C /\ ( F ` A ) e. |^| { x | ph } ) <-> ( A e. C /\ A. x ( ph -> ( F ` A ) e. x ) ) )
6	2	baibr	|- ( A e. C -> ( ( F ` A ) e. x <-> A e. E ) )
7	6	imbi2d	|- ( A e. C -> ( ( ph -> ( F ` A ) e. x ) <-> ( ph -> A e. E ) ) )
8	7	albidv	|- ( A e. C -> ( A. x ( ph -> ( F ` A ) e. x ) <-> A. x ( ph -> A e. E ) ) )
9	8	pm5.32i	|- ( ( A e. C /\ A. x ( ph -> ( F ` A ) e. x ) ) <-> ( A e. C /\ A. x ( ph -> A e. E ) ) )
10	1 5 9	3bitri	|- ( A e. B <-> ( A e. C /\ A. x ( ph -> A e. E ) ) )