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

Definition df-txp 25698
Description: Define the tail cross of two classes. Membership in this class is defined by txpss3v 25723 and brtxp 25725. (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 25674 . 2  class  ( A 
(x)  B )
4 c1st 6347 . . . . . 6  class  1st
5 cvv 2956 . . . . . . 7  class  _V
65, 5cxp 4876 . . . . . 6  class  ( _V 
X.  _V )
74, 6cres 4880 . . . . 5  class  ( 1st  |`  ( _V  X.  _V ) )
87ccnv 4877 . . . 4  class  `' ( 1st  |`  ( _V  X.  _V ) )
98, 1ccom 4882 . . 3  class  ( `' ( 1st  |`  ( _V  X.  _V ) )  o.  A )
10 c2nd 6348 . . . . . 6  class  2nd
1110, 6cres 4880 . . . . 5  class  ( 2nd  |`  ( _V  X.  _V ) )
1211ccnv 4877 . . . 4  class  `' ( 2nd  |`  ( _V  X.  _V ) )
1312, 2ccom 4882 . . 3  class  ( `' ( 2nd  |`  ( _V  X.  _V ) )  o.  B )
149, 13cin 3319 . 2  class  ( ( `' ( 1st  |`  ( _V  X.  _V ) )  o.  A )  i^i  ( `' ( 2nd  |`  ( _V  X.  _V ) )  o.  B
) )
153, 14wceq 1652 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  25723  brtxp  25725  dfpprod2  25727
  Copyright terms: Public domain W3C validator