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

Definition df-xp 4274
 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 4266 . 2 class (A × B)
4 vx . . . . . 6 setvar x
54cv 1225 . . . . 5 class x
65, 1wcel 1370 . . . 4 wff x A
7 vy . . . . . 6 setvar y
87cv 1225 . . . . 5 class y
98, 2wcel 1370 . . . 4 wff y B
106, 9wa 97 . . 3 wff (x A y B)
1110, 4, 7copab 3787 . 2 class {⟨x, y⟩ ∣ (x A y B)}
123, 11wceq 1226 1 wff (A × B) = {⟨x, y⟩ ∣ (x A y B)}
 Colors of variables: wff set class This definition is referenced by:  xpeq1  4282  xpeq2  4283  elxpi  4284  elxp  4285  nfxp  4294  fconstmpt  4310  brab2a  4316  xpundi  4319  xpundir  4320  opabssxp  4337  csbxpg  4344  xpss12  4368  inxp  4393  dmxpm  4478  resopab  4575  cnvxp  4665  xpcom  4787  dfxp3  5739  dmaddpq  6232  dmmulpq  6233  enq0enq  6280  npsspw  6319
 Copyright terms: Public domain W3C validator