Theorem elimaint

Description: Element of image of intersection. (Contributed by RP, 13-Apr-2020)

	Ref	Expression
Assertion	elimaint	|- ( y e. ( |^| A " B ) <-> E. b e. B A. a e. A <. b , y >. e. a )

Proof

Step	Hyp	Ref	Expression
1		vex	|- y e. _V
2	1	elima	|- ( y e. ( |^| A " B ) <-> E. b e. B b |^| A y )
3		df-br	|- ( b |^| A y <-> <. b , y >. e. |^| A )
4		opex	|- <. b , y >. e. _V
5	4	elint2	|- ( <. b , y >. e. |^| A <-> A. a e. A <. b , y >. e. a )
6	3 5	bitri	|- ( b |^| A y <-> A. a e. A <. b , y >. e. a )
7	6	rexbii	|- ( E. b e. B b |^| A y <-> E. b e. B A. a e. A <. b , y >. e. a )
8	2 7	bitri	|- ( y e. ( |^| A " B ) <-> E. b e. B A. a e. A <. b , y >. e. a )