Definition df-pprod 5739

Description: Define the parallel product operation. (Contributed by SF, 9-Feb-2015.)

Assertion

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

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 5738	. 2 class PProd (A, B)
4		c1st 4718	. . . 4 class 1st
5	1, 4	ccom 4722	. . 3 class (A o. 1st)
6		c2nd 4784	. . . 4 class 2nd
7	2, 6	ccom 4722	. . 3 class (B o. 2nd)
8	5, 7	ctxp 5736	. 2 class ((A o. 1st) (x) (B o. 2nd))
9	3, 8	wceq 1642	1 wff PProd (A, B) = ((A o. 1st) (x) (B o. 2nd))

This definition is referenced by:  pprodeq1  5835  pprodeq2  5836  qrpprod  5837  pprodexg  5838  brpprod  5840  cnvpprod  5842