Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-xrn Structured version   Visualization version   GIF version

Definition df-xrn 35503
Description: Define the range Cartesian product of two classes. Definition from [Holmes] p. 40. Membership in this class is characterized by xrnss3v 35504 and brxrn 35506. This is Scott Fenton's df-txp 33212 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 33212. (Contributed by Scott Fenton, 31-Mar-2012.)
Assertion
Ref Expression
df-xrn (𝐴𝐵) = (((1st ↾ (V × V)) ∘ 𝐴) ∩ ((2nd ↾ (V × V)) ∘ 𝐵))

Detailed syntax breakdown of Definition df-xrn
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cxrn 35333 . 2 class (𝐴𝐵)
4 c1st 7676 . . . . . 6 class 1st
5 cvv 3492 . . . . . . 7 class V
65, 5cxp 5546 . . . . . 6 class (V × V)
74, 6cres 5550 . . . . 5 class (1st ↾ (V × V))
87ccnv 5547 . . . 4 class (1st ↾ (V × V))
98, 1ccom 5552 . . 3 class ((1st ↾ (V × V)) ∘ 𝐴)
10 c2nd 7677 . . . . . 6 class 2nd
1110, 6cres 5550 . . . . 5 class (2nd ↾ (V × V))
1211ccnv 5547 . . . 4 class (2nd ↾ (V × V))
1312, 2ccom 5552 . . 3 class ((2nd ↾ (V × V)) ∘ 𝐵)
149, 13cin 3932 . 2 class (((1st ↾ (V × V)) ∘ 𝐴) ∩ ((2nd ↾ (V × V)) ∘ 𝐵))
153, 14wceq 1528 1 wff (𝐴𝐵) = (((1st ↾ (V × V)) ∘ 𝐴) ∩ ((2nd ↾ (V × V)) ∘ 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  xrnss3v  35504  brxrn  35506  xrneq1  35509  xrneq2  35512  xrnres  35530  xrnres2  35531  xrnres3  35532
  Copyright terms: Public domain W3C validator