Definition df-xrn 34134

Description: Define the range Cartesian product, or range cross of two classes. Definition from [Holmes] p. 40. Membership in this class is defined by xrnss3v 34135 and ~? brxrn . This is Scott Fenton's df-txp 31961 with different symbols, cf. https://github.com/metamath/set.mm/issues/2469 . (Contributed by Scott Fenton, 31-Mar-2012.)

Assertion

Ref	Expression
df-xrn	|- ( A |X. B ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) )

Detailed syntax breakdown of Definition df-xrn

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cxrn 33982	. 2 class ( A |X. B )
4		c1st 7166	. . . . . 6 class 1st
5		cvv 3200	. . . . . . 7 class _V
6	5, 5	cxp 5112	. . . . . 6 class ( _V X. _V )
7	4, 6	cres 5116	. . . . 5 class ( 1st |` ( _V X. _V ) )
8	7	ccnv 5113	. . . 4 class `' ( 1st |` ( _V X. _V ) )
9	8, 1	ccom 5118	. . 3 class ( `' ( 1st |` ( _V X. _V ) ) o. A )
10		c2nd 7167	. . . . . 6 class 2nd
11	10, 6	cres 5116	. . . . 5 class ( 2nd |` ( _V X. _V ) )
12	11	ccnv 5113	. . . 4 class `' ( 2nd |` ( _V X. _V ) )
13	12, 2	ccom 5118	. . 3 class ( `' ( 2nd |` ( _V X. _V ) ) o. B )
14	9, 13	cin 3573	. 2 class ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) )
15	3, 14	wceq 1483	1 wff ( A |X. B ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) )

This definition is referenced by:  xrnss3v  34135