NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-txp Unicode version

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

Detailed syntax breakdown of Definition df-txp
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2ctxp 5735 . 2
4 c1st 4717 . . . . 5
54ccnv 4771 . . . 4
65, 1ccom 4721 . . 3
7 c2nd 4783 . . . . 5
87ccnv 4771 . . . 4
98, 2ccom 4721 . . 3
106, 9cin 3208 . 2
113, 10wceq 1642 1
Colors of variables: wff setvar class
This definition is referenced by:  txpeq1  5779  txpeq2  5780  trtxp  5781  brtxp  5783  txpexg  5784  cnvpprod  5841
  Copyright terms: Public domain W3C validator