Definition df-pprod 5738

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 5737	. 2 class PProd (A, B)
4		c1st 4717	. . . 4 class 1st
5	1, 4	ccom 4721	. . 3 class (A o. 1st)
6		c2nd 4783	. . . 4 class 2nd
7	2, 6	ccom 4721	. . 3 class (B o. 2nd)
8	5, 7	ctxp 5735	. 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  5834  pprodeq2  5835  qrpprod  5836  pprodexg  5837  brpprod  5839  cnvpprod  5841