Theorem opelxpii

Description: Ordered pair membership in a Cartesian product (implication), induction form. (Contributed by Steven Nguyen, 17-Jul-2022)

	Ref	Expression
Hypotheses	opelxpii.1	|- A e. C
	opelxpii.2	|- B e. D
Assertion	opelxpii	|- <. A , B >. e. ( C X. D )

Proof

Step	Hyp	Ref	Expression
1		opelxpii.1	|- A e. C
2		opelxpii.2	|- B e. D
3		opelxpi	|- ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) )
4	1 2 3	mp2an	|- <. A , B >. e. ( C X. D )