Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-altxp Unicode version

Definition df-altxp 24493
Description: Define cross products of alternative ordered pairs. (Contributed by Scott Fenton, 23-Mar-2012.)
Assertion
Ref Expression
df-altxp  |-  ( A 
XX.  B )  =  { z  |  E. x  e.  A  E. y  e.  B  z  =  << x ,  y
>> }
Distinct variable groups:    x, A, y, z    x, B, y, z

Detailed syntax breakdown of Definition df-altxp
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2caltxp 24491 . 2  class  ( A 
XX.  B )
4 vz . . . . . . 7  set  z
54cv 1622 . . . . . 6  class  z
6 vx . . . . . . . 8  set  x
76cv 1622 . . . . . . 7  class  x
8 vy . . . . . . . 8  set  y
98cv 1622 . . . . . . 7  class  y
107, 9caltop 24490 . . . . . 6  class  << x ,  y >>
115, 10wceq 1623 . . . . 5  wff  z  = 
<< x ,  y >>
1211, 8, 2wrex 2544 . . . 4  wff  E. y  e.  B  z  =  << x ,  y >>
1312, 6, 1wrex 2544 . . 3  wff  E. x  e.  A  E. y  e.  B  z  =  << x ,  y >>
1413, 4cab 2269 . 2  class  { z  |  E. x  e.  A  E. y  e.  B  z  =  << x ,  y >> }
153, 14wceq 1623 1  wff  ( A 
XX.  B )  =  { z  |  E. x  e.  A  E. y  e.  B  z  =  << x ,  y
>> }
Colors of variables: wff set class
This definition is referenced by:  altxpeq1  24507  altxpeq2  24508  elaltxp  24509
  Copyright terms: Public domain W3C validator