Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-xp Unicode version

Definition df-xp 4557
 Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. For example, ( { 1 , 5 } { 2 , 7 } ) = ( { 1 , 2 , 1 , 7 } { 5 , 2 , 5 , 7 } ) . Another example is that the set of rational numbers are defined in using the cross-product ( Z N ) ; the left- and right-hand sides of the cross-product represent the top (integer) and bottom (natural) numbers of a fraction. (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-xp
Distinct variable groups:   ,,   ,,

Detailed syntax breakdown of Definition df-xp
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cxp 4549 . 2
4 vx . . . . . 6
54cv 1331 . . . . 5
65, 1wcel 1481 . . . 4
7 vy . . . . . 6
87cv 1331 . . . . 5
98, 2wcel 1481 . . . 4
106, 9wa 103 . . 3
1110, 4, 7copab 3998 . 2
123, 11wceq 1332 1
 Colors of variables: wff set class This definition is referenced by:  xpeq1  4565  xpeq2  4566  elxpi  4567  elxp  4568  nfxp  4578  fconstmpt  4598  brab2a  4604  xpundi  4607  xpundir  4608  opabssxp  4625  csbxpg  4632  xpss12  4658  inxp  4685  dmxpm  4771  dmxpid  4772  resopab  4875  cnvxp  4969  xpcom  5097  dfxp3  6104  dmaddpq  7240  dmmulpq  7241  enq0enq  7292  npsspw  7332  shftfvalg  10651  shftfval  10654
 Copyright terms: Public domain W3C validator