Definition df-txp 5737

Description: Define the tail cross product of two classes. Definition from [Holmes] p. 40. See brtxp 5784 for membership. (Contributed by SF, 9-Feb-2015.)

Assertion

Ref	Expression
df-txp	|- (A (x) B) = ((`'1st o. A) i^i (`'2nd o. B))

Detailed syntax breakdown of Definition df-txp

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	ctxp 5736	. 2 class (A (x) B)
4		c1st 4718	. . . . 5 class 1st
5	4	ccnv 4772	. . . 4 class `'1st
6	5, 1	ccom 4722	. . 3 class (`'1st o. A)
7		c2nd 4784	. . . . 5 class 2nd
8	7	ccnv 4772	. . . 4 class `'2nd
9	8, 2	ccom 4722	. . 3 class (`'2nd o. B)
10	6, 9	cin 3209	. 2 class ((`'1st o. A) i^i (`'2nd o. B))
11	3, 10	wceq 1642	1 wff (A (x) B) = ((`'1st o. A) i^i (`'2nd o. B))

This definition is referenced by:  txpeq1  5780  txpeq2  5781  trtxp  5782  brtxp  5784  txpexg  5785  cnvpprod  5842