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

Definition df-altxp 24565
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 24563 . 2  class  ( A 
XX.  B )
4 vz . . . . . . 7  set  z
54cv 1631 . . . . . 6  class  z
6 vx . . . . . . . 8  set  x
76cv 1631 . . . . . . 7  class  x
8 vy . . . . . . . 8  set  y
98cv 1631 . . . . . . 7  class  y
107, 9caltop 24562 . . . . . 6  class  << x ,  y >>
115, 10wceq 1632 . . . . 5  wff  z  = 
<< x ,  y >>
1211, 8, 2wrex 2557 . . . 4  wff  E. y  e.  B  z  =  << x ,  y >>
1312, 6, 1wrex 2557 . . 3  wff  E. x  e.  A  E. y  e.  B  z  =  << x ,  y >>
1413, 4cab 2282 . 2  class  { z  |  E. x  e.  A  E. y  e.  B  z  =  << x ,  y >> }
153, 14wceq 1632 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  24579  altxpeq2  24580  elaltxp  24581
  Copyright terms: Public domain W3C validator