Definition df-txp

Description: Define the tail cross of two classes. Membership in this class is defined by txpss3v and brtxp . (Contributed by Scott Fenton, 31-Mar-2012)

	Ref	Expression
Assertion	df-txp	|- ( A (x) B ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	ctxp	|- ( A (x) B )
3		c1st	|- 1st
4		cvv	|- _V
5	4 4	cxp	|- ( _V X. _V )
6	3 5	cres	|- ( 1st |` ( _V X. _V ) )
7	6	ccnv	|- `' ( 1st |` ( _V X. _V ) )
8	7 0	ccom	|- ( `' ( 1st |` ( _V X. _V ) ) o. A )
9		c2nd	|- 2nd
10	9 5	cres	|- ( 2nd |` ( _V X. _V ) )
11	10	ccnv	|- `' ( 2nd |` ( _V X. _V ) )
12	11 1	ccom	|- ( `' ( 2nd |` ( _V X. _V ) ) o. B )
13	8 12	cin	|- ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) )
14	2 13	wceq	|- ( A (x) B ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) )