NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-txp GIF 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 (AB) = ((1st A) ∩ (2nd B))

Detailed syntax breakdown of Definition df-txp
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2ctxp 5735 . 2 class (AB)
4 c1st 4717 . . . . 5 class 1st
54ccnv 4771 . . . 4 class 1st
65, 1ccom 4721 . . 3 class (1st A)
7 c2nd 4783 . . . . 5 class 2nd
87ccnv 4771 . . . 4 class 2nd
98, 2ccom 4721 . . 3 class (2nd B)
106, 9cin 3208 . 2 class ((1st A) ∩ (2nd B))
113, 10wceq 1642 1 wff (AB) = ((1st A) ∩ (2nd B))
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