NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-pprod Unicode version

Definition df-pprod 5738
Description: Define the parallel product operation. (Contributed by SF, 9-Feb-2015.)
Assertion
Ref Expression
df-pprod PProd

Detailed syntax breakdown of Definition df-pprod
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cpprod 5737 . 2 PProd
4 c1st 4717 . . . 4
51, 4ccom 4721 . . 3
6 c2nd 4783 . . . 4
72, 6ccom 4721 . . 3
85, 7ctxp 5735 . 2
93, 8wceq 1642 1 PProd
Colors of variables: wff setvar class
This definition is referenced by:  pprodeq1  5834  pprodeq2  5835  qrpprod  5836  pprodexg  5837  brpprod  5839  cnvpprod  5841
  Copyright terms: Public domain W3C validator