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

Definition df-xp 4266
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 (A × B) = {⟨x, y⟩ ∣ (x A y B)}
Distinct variable groups:   x,y,A   x,B,y

Detailed syntax breakdown of Definition df-xp
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2cxp 4258 . 2 class (A × B)
4 vx . . . . . 6 setvar x
54cv 1222 . . . . 5 class x
65, 1wcel 1366 . . . 4 wff x A
7 vy . . . . . 6 setvar y
87cv 1222 . . . . 5 class y
98, 2wcel 1366 . . . 4 wff y B
106, 9wa 97 . . 3 wff (x A y B)
1110, 4, 7copab 3780 . 2 class {⟨x, y⟩ ∣ (x A y B)}
123, 11wceq 1223 1 wff (A × B) = {⟨x, y⟩ ∣ (x A y B)}
Colors of variables: wff set class
This definition is referenced by:  xpeq1  4274  xpeq2  4275  elxpi  4276  elxp  4277  nfxp  4286  fconstmpt  4302  brab2a  4308  xpundi  4311  xpundir  4312  opabssxp  4329  csbxpg  4336  xpss12  4360  inxp  4385  dmxpm  4470  resopab  4567  cnvxp  4657  xpcom  4779  dfxp3  5731  dmaddpq  6224  dmmulpq  6225  enq0enq  6272  npsspw  6311
  Copyright terms: Public domain W3C validator