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

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 1st ) ⊗ (B 2nd ))

Detailed syntax breakdown of Definition df-pprod
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2cpprod 5737 . 2 class PProd (A, B)
4 c1st 4717 . . . 4 class 1st
51, 4ccom 4721 . . 3 class (A 1st )
6 c2nd 4783 . . . 4 class 2nd
72, 6ccom 4721 . . 3 class (B 2nd )
85, 7ctxp 5735 . 2 class ((A 1st ) ⊗ (B 2nd ))
93, 8wceq 1642 1 wff PProd (A, B) = ((A 1st ) ⊗ (B 2nd ))
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