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 30569
Description: Define the tail cross of two classes. Membership in this class is defined by txpss3v 30594 and brtxp 30596. (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 30545 . 2  class  ( A 
(x)  B )
4 c1st 6749 . . . . . 6  class  1st
5 cvv 3022 . . . . . . 7  class  _V
65, 5cxp 4794 . . . . . 6  class  ( _V 
X.  _V )
74, 6cres 4798 . . . . 5  class  ( 1st  |`  ( _V  X.  _V ) )
87ccnv 4795 . . . 4  class  `' ( 1st  |`  ( _V  X.  _V ) )
98, 1ccom 4800 . . 3  class  ( `' ( 1st  |`  ( _V  X.  _V ) )  o.  A )
10 c2nd 6750 . . . . . 6  class  2nd
1110, 6cres 4798 . . . . 5  class  ( 2nd  |`  ( _V  X.  _V ) )
1211ccnv 4795 . . . 4  class  `' ( 2nd  |`  ( _V  X.  _V ) )
1312, 2ccom 4800 . . 3  class  ( `' ( 2nd  |`  ( _V  X.  _V ) )  o.  B )
149, 13cin 3378 . 2  class  ( ( `' ( 1st  |`  ( _V  X.  _V ) )  o.  A )  i^i  ( `' ( 2nd  |`  ( _V  X.  _V ) )  o.  B
) )
153, 14wceq 1437 1  wff  ( A 
(x)  B )  =  ( ( `' ( 1st  |`  ( _V  X.  _V ) )  o.  A )  i^i  ( `' ( 2nd  |`  ( _V  X.  _V ) )  o.  B ) )
Colors of variables: wff setvar class
This definition is referenced by:  txpss3v  30594  brtxp  30596  dfpprod2  30598
  Copyright terms: Public domain W3C validator