Definition df-txp 5736

Description: Define the tail cross product of two classes. Definition from [Holmes] p. 40. See brtxp 5783 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 5735	. 2 class (A (x) B)
4		c1st 4717	. . . . 5 class 1st
5	4	ccnv 4771	. . . 4 class `'1st
6	5, 1	ccom 4721	. . 3 class (`'1st o. A)
7		c2nd 4783	. . . . 5 class 2nd
8	7	ccnv 4771	. . . 4 class `'2nd
9	8, 2	ccom 4721	. . 3 class (`'2nd o. B)
10	6, 9	cin 3208	. 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  5779  txpeq2  5780  trtxp  5781  brtxp  5783  txpexg  5784  cnvpprod  5841