Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-txp Unicode version

Definition df-txp 24466
Description: Define the tail cross of two classes. Membership in this class is defined by txpss3v 24489 and brtxp 24491. (Contributed by Scott Fenton, 31-Mar-2012.)
Assertion
Ref Expression
df-txp  |-  ( A 
(x)  B )  =  ( ( `' ( 1st  |`  ( _V  X.  _V ) )  o.  A )  i^i  ( `' ( 2nd  |`  ( _V  X.  _V ) )  o.  B ) )

Detailed syntax breakdown of Definition df-txp
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2ctxp 24444 . 2  class  ( A 
(x)  B )
4 c1st 6136 . . . . . 6  class  1st
5 cvv 2801 . . . . . . 7  class  _V
65, 5cxp 4703 . . . . . 6  class  ( _V 
X.  _V )
74, 6cres 4707 . . . . 5  class  ( 1st  |`  ( _V  X.  _V ) )
87ccnv 4704 . . . 4  class  `' ( 1st  |`  ( _V  X.  _V ) )
98, 1ccom 4709 . . 3  class  ( `' ( 1st  |`  ( _V  X.  _V ) )  o.  A )
10 c2nd 6137 . . . . . 6  class  2nd
1110, 6cres 4707 . . . . 5  class  ( 2nd  |`  ( _V  X.  _V ) )
1211ccnv 4704 . . . 4  class  `' ( 2nd  |`  ( _V  X.  _V ) )
1312, 2ccom 4709 . . 3  class  ( `' ( 2nd  |`  ( _V  X.  _V ) )  o.  B )
149, 13cin 3164 . 2  class  ( ( `' ( 1st  |`  ( _V  X.  _V ) )  o.  A )  i^i  ( `' ( 2nd  |`  ( _V  X.  _V ) )  o.  B
) )
153, 14wceq 1632 1  wff  ( A 
(x)  B )  =  ( ( `' ( 1st  |`  ( _V  X.  _V ) )  o.  A )  i^i  ( `' ( 2nd  |`  ( _V  X.  _V ) )  o.  B ) )
Colors of variables: wff set class
This definition is referenced by:  txpss3v  24489  brtxp  24491  dfpprod2  24493
  Copyright terms: Public domain W3C validator