Definition df-pprod 31962

Description: Define the parallel product of two classes. Membership in this class is defined by pprodss4v 31991 and brpprod 31992. (Contributed by Scott Fenton, 11-Apr-2014.)

Assertion

Ref	Expression
df-pprod	|- pprod ( A , B ) = ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) )

Detailed syntax breakdown of Definition df-pprod

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cpprod 31938	. 2 class pprod ( A , B )
4		c1st 7166	. . . . 5 class 1st
5		cvv 3200	. . . . . 6 class _V
6	5, 5	cxp 5112	. . . . 5 class ( _V X. _V )
7	4, 6	cres 5116	. . . 4 class ( 1st |` ( _V X. _V ) )
8	1, 7	ccom 5118	. . 3 class ( A o. ( 1st |` ( _V X. _V ) ) )
9		c2nd 7167	. . . . 5 class 2nd
10	9, 6	cres 5116	. . . 4 class ( 2nd |` ( _V X. _V ) )
11	2, 10	ccom 5118	. . 3 class ( B o. ( 2nd |` ( _V X. _V ) ) )
12	8, 11	ctxp 31937	. 2 class ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) )
13	3, 12	wceq 1483	1 wff pprod ( A , B ) = ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) )

This definition is referenced by:  dfpprod2  31989  pprodss4v  31991  brpprod  31992