Definition df-rn 2429

Description: Define the range of a class. For an alternate definition, see dfrn2 2523.

Assertion

Ref	Expression
df-rn	⊢ ran A = dom ◡A

Detailed syntax breakdown of Definition df-rn

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	crn 2411	. 2 class ran A
3	1	ccnv 2409	. . 3 class ◡A
4	3	cdm 2410	. 2 class dom ◡A
5	2, 4	wceq 1091	1 wff ran A = dom ◡A

This definition is referenced by:  dfrn2 2523  rneq 2555  rnss 2558  brelrn 2559  rnco 2571  rncoeq 2574  rnsnop 2637  op2nda 2639  rnun 2644  rnin 2645  rnxp 2657  cnvexg 2669  funcnvres 2710  funimacnv 2711  fconst 2774  f1cnv 2782  f1o4 2807  f1ocnv 2811  tz7.48-3 2996  sbthlem5 3353  sbthlem8 3356  sbthlem9 3357  inf3lem7 3470  zornlem4 3606  fodom 3613  fodomb 3615  uzrdgval 4657

metamath.org