New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-xp | Unicode version |
Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. (Contributed by SF, 5-Jan-2015.) |
Ref | Expression |
---|---|
df-xp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | cxp 4770 | . 2 |
4 | vx | . . . . . 6 | |
5 | 4 | cv 1641 | . . . . 5 |
6 | 5, 1 | wcel 1710 | . . . 4 |
7 | vy | . . . . . 6 | |
8 | 7 | cv 1641 | . . . . 5 |
9 | 8, 2 | wcel 1710 | . . . 4 |
10 | 6, 9 | wa 358 | . . 3 |
11 | 10, 4, 7 | copab 4622 | . 2 |
12 | 3, 11 | wceq 1642 | 1 |
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 |