Theorem bj-elinxp

Description: Membership in an intersection with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022) Use the x R y idiom and give a shorter proof not depending on df-rel . (Revised by BJ, 16-Oct-2026) Note to remove when moving to main section: a shortening of the exact statement elinxp is possible along the same line.

	Ref	Expression
Assertion	bj-elinxp	|- ( C e. ( R i^i ( A X. B ) ) <-> E. x e. A E. y e. B ( C = <. x , y >. /\ x R y ) )

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( C e. ( R i^i ( A X. B ) ) <-> ( C e. R /\ C e. ( A X. B ) ) )
2		elxp2	|- ( C e. ( A X. B ) <-> E. x e. A E. y e. B C = <. x , y >. )
3	2	anbi2i	|- ( ( C e. R /\ C e. ( A X. B ) ) <-> ( C e. R /\ E. x e. A E. y e. B C = <. x , y >. ) )
4		r19.42v	|- ( E. y e. B ( C e. R /\ C = <. x , y >. ) <-> ( C e. R /\ E. y e. B C = <. x , y >. ) )
5	4	rexbii	|- ( E. x e. A E. y e. B ( C e. R /\ C = <. x , y >. ) <-> E. x e. A ( C e. R /\ E. y e. B C = <. x , y >. ) )
6		eleq1	|- ( C = <. x , y >. -> ( C e. R <-> <. x , y >. e. R ) )
7		df-br	|- ( x R y <-> <. x , y >. e. R )
8	6 7	bitr4di	|- ( C = <. x , y >. -> ( C e. R <-> x R y ) )
9	8	pm5.32ri	|- ( ( C e. R /\ C = <. x , y >. ) <-> ( x R y /\ C = <. x , y >. ) )
10	9	biancomi	|- ( ( C e. R /\ C = <. x , y >. ) <-> ( C = <. x , y >. /\ x R y ) )
11	10	rexbii	|- ( E. y e. B ( C e. R /\ C = <. x , y >. ) <-> E. y e. B ( C = <. x , y >. /\ x R y ) )
12	11	rexbii	|- ( E. x e. A E. y e. B ( C e. R /\ C = <. x , y >. ) <-> E. x e. A E. y e. B ( C = <. x , y >. /\ x R y ) )
13		r19.42v	|- ( E. x e. A ( C e. R /\ E. y e. B C = <. x , y >. ) <-> ( C e. R /\ E. x e. A E. y e. B C = <. x , y >. ) )
14	5 12 13	3bitr3ri	|- ( ( C e. R /\ E. x e. A E. y e. B C = <. x , y >. ) <-> E. x e. A E. y e. B ( C = <. x , y >. /\ x R y ) )
15	1 3 14	3bitri	|- ( C e. ( R i^i ( A X. B ) ) <-> E. x e. A E. y e. B ( C = <. x , y >. /\ x R y ) )