Theorem elxp6

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 . (Contributed by NM, 9-Oct-2004)

	Ref	Expression
Assertion	elxp6	|- ( A e. ( B X. C ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )

Proof

Step	Hyp	Ref	Expression
1		elxp4	|- ( A e. ( B X. C ) <-> ( A = <. U. dom { A } , U. ran { A } >. /\ ( U. dom { A } e. B /\ U. ran { A } e. C ) ) )
2		1stval	|- ( 1st ` A ) = U. dom { A }
3		2ndval	|- ( 2nd ` A ) = U. ran { A }
4	2 3	opeq12i	|- <. ( 1st ` A ) , ( 2nd ` A ) >. = <. U. dom { A } , U. ran { A } >.
5	4	eqeq2i	|- ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. <-> A = <. U. dom { A } , U. ran { A } >. )
6	2	eleq1i	|- ( ( 1st ` A ) e. B <-> U. dom { A } e. B )
7	3	eleq1i	|- ( ( 2nd ` A ) e. C <-> U. ran { A } e. C )
8	6 7	anbi12i	|- ( ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) <-> ( U. dom { A } e. B /\ U. ran { A } e. C ) )
9	5 8	anbi12i	|- ( ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) <-> ( A = <. U. dom { A } , U. ran { A } >. /\ ( U. dom { A } e. B /\ U. ran { A } e. C ) ) )
10	1 9	bitr4i	|- ( A e. ( B X. C ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )