New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-xp GIF version

Definition df-xp 4784
 Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. (Contributed by SF, 5-Jan-2015.)
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 4770 . 2 class (A × B)
4 vx . . . . . 6 setvar x
54cv 1641 . . . . 5 class x
65, 1wcel 1710 . . . 4 wff x A
7 vy . . . . . 6 setvar y
87cv 1641 . . . . 5 class y
98, 2wcel 1710 . . . 4 wff y B
106, 9wa 358 . . 3 wff (x A y B)
1110, 4, 7copab 4622 . 2 class {x, y (x A y B)}
123, 11wceq 1642 1 wff (A × B) = {x, y (x A y B)}
 Colors of variables: wff setvar class This definition is referenced by:  xpeq1  4798  xpeq2  4799  elxpi  4800  elxp  4801  nfxp  4810  csbxpg  4813  fconstopab  4815  xpundi  4832  xpundir  4833  opabssxp  4837  xpss12  4855  inxp  4863  dmxp  4923  resopab  4999  cnvxp  5043  ovg  5601  composefn  5818  fnce  6176
 Copyright terms: Public domain W3C validator