Metamath Proof Explorer


Definition df-xrn

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 AB=1stV×V-1A2ndV×V-1B

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA classA
1 cB classB
2 0 1 cxrn classAB
3 c1st class1st
4 cvv classV
5 4 4 cxp classV×V
6 3 5 cres class1stV×V
7 6 ccnv class1stV×V-1
8 7 0 ccom class1stV×V-1A
9 c2nd class2nd
10 9 5 cres class2ndV×V
11 10 ccnv class2ndV×V-1
12 11 1 ccom class2ndV×V-1B
13 8 12 cin class1stV×V-1A2ndV×V-1B
14 2 13 wceq wffAB=1stV×V-1A2ndV×V-1B