Metamath Proof Explorer

Theorem elinintrab

Description: Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 14-Aug-2020)

		Ref	Expression
	Assertion	elinintrab	\|- ( A e. V -> ( A e. \|^\| { w e. ~P B \| E. x ( w = ( B i^i x ) /\ ph ) } <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		vex	\|- x e. _V
2	1	inex2	\|- ( B i^i x ) e. _V
3		inss1	\|- ( B i^i x ) C_ B
4	2 3	elmapintrab	\|- ( A e. V -> ( A e. \|^\| { w e. ~P B \| E. x ( w = ( B i^i x ) /\ ph ) } <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. ( B i^i x ) ) ) ) )
5		elin	\|- ( A e. ( B i^i x ) <-> ( A e. B /\ A e. x ) )
6	5	imbi2i	\|- ( ( ph -> A e. ( B i^i x ) ) <-> ( ph -> ( A e. B /\ A e. x ) ) )
7		jcab	\|- ( ( ph -> ( A e. B /\ A e. x ) ) <-> ( ( ph -> A e. B ) /\ ( ph -> A e. x ) ) )
8	6 7	bitri	\|- ( ( ph -> A e. ( B i^i x ) ) <-> ( ( ph -> A e. B ) /\ ( ph -> A e. x ) ) )
9	8	albii	\|- ( A. x ( ph -> A e. ( B i^i x ) ) <-> A. x ( ( ph -> A e. B ) /\ ( ph -> A e. x ) ) )
10		19.26	\|- ( A. x ( ( ph -> A e. B ) /\ ( ph -> A e. x ) ) <-> ( A. x ( ph -> A e. B ) /\ A. x ( ph -> A e. x ) ) )
11		19.23v	\|- ( A. x ( ph -> A e. B ) <-> ( E. x ph -> A e. B ) )
12	11	anbi1i	\|- ( ( A. x ( ph -> A e. B ) /\ A. x ( ph -> A e. x ) ) <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. x ) ) )
13	10 12	bitri	\|- ( A. x ( ( ph -> A e. B ) /\ ( ph -> A e. x ) ) <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. x ) ) )
14	9 13	bitri	\|- ( A. x ( ph -> A e. ( B i^i x ) ) <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. x ) ) )
15	14	anbi2i	\|- ( ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. ( B i^i x ) ) ) <-> ( ( E. x ph -> A e. B ) /\ ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. x ) ) ) )
16		anabs5	\|- ( ( ( E. x ph -> A e. B ) /\ ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. x ) ) ) <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. x ) ) )
17	15 16	bitri	\|- ( ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. ( B i^i x ) ) ) <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. x ) ) )
18	4 17	bitrdi	\|- ( A e. V -> ( A e. \|^\| { w e. ~P B \| E. x ( w = ( B i^i x ) /\ ph ) } <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. x ) ) ) )