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

Definition df-altxp 28127
Description: Define Cartesian 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 28125 . 2  class  ( A 
XX.  B )
4 vz . . . . . . 7  setvar  z
54cv 1369 . . . . . 6  class  z
6 vx . . . . . . . 8  setvar  x
76cv 1369 . . . . . . 7  class  x
8 vy . . . . . . . 8  setvar  y
98cv 1369 . . . . . . 7  class  y
107, 9caltop 28124 . . . . . 6  class  << x ,  y >>
115, 10wceq 1370 . . . . 5  wff  z  = 
<< x ,  y >>
1211, 8, 2wrex 2796 . . . 4  wff  E. y  e.  B  z  =  << x ,  y >>
1312, 6, 1wrex 2796 . . 3  wff  E. x  e.  A  E. y  e.  B  z  =  << x ,  y >>
1413, 4cab 2436 . 2  class  { z  |  E. x  e.  A  E. y  e.  B  z  =  << x ,  y >> }
153, 14wceq 1370 1  wff  ( A 
XX.  B )  =  { z  |  E. x  e.  A  E. y  e.  B  z  =  << x ,  y
>> }
Colors of variables: wff setvar class
This definition is referenced by:  altxpeq1  28141  altxpeq2  28142  elaltxp  28143
  Copyright terms: Public domain W3C validator