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

Definition df-xp 4552
 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 class 𝐴
2 cB . . 3 class 𝐵
31, 2cxp 4544 . 2 class (𝐴 × 𝐵)
4 vx . . . . . 6 setvar 𝑥
54cv 1331 . . . . 5 class 𝑥
65, 1wcel 1481 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1331 . . . . 5 class 𝑦
98, 2wcel 1481 . . . 4 wff 𝑦𝐵
106, 9wa 103 . . 3 wff (𝑥𝐴𝑦𝐵)
1110, 4, 7copab 3995 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
123, 11wceq 1332 1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
 Colors of variables: wff set class This definition is referenced by:  xpeq1  4560  xpeq2  4561  elxpi  4562  elxp  4563  nfxp  4573  fconstmpt  4593  brab2a  4599  xpundi  4602  xpundir  4603  opabssxp  4620  csbxpg  4627  xpss12  4653  inxp  4680  dmxpm  4766  dmxpid  4767  resopab  4870  cnvxp  4964  xpcom  5092  dfxp3  6099  dmaddpq  7210  dmmulpq  7211  enq0enq  7262  npsspw  7302  shftfvalg  10621  shftfval  10624
 Copyright terms: Public domain W3C validator