Description: Define the range Cartesian product of two classes. Definition from Holmes p. 40. Membership in this class is characterized by xrnss3v and brxrn . This is Scott Fenton's df-txp with a different symbol, see https://github.com/metamath/set.mm/issues/2469 . (Contributed by Scott Fenton, 31-Mar-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | df-xrn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cA | |
|
1 | cB | |
|
2 | 0 1 | cxrn | |
3 | c1st | |
|
4 | cvv | |
|
5 | 4 4 | cxp | |
6 | 3 5 | cres | |
7 | 6 | ccnv | |
8 | 7 0 | ccom | |
9 | c2nd | |
|
10 | 9 5 | cres | |
11 | 10 | ccnv | |
12 | 11 1 | ccom | |
13 | 8 12 | cin | |
14 | 2 13 | wceq | |