Definition df-rn 3270

Description: Define the range of a class. For an alternate definitions, see dfrn2 3394, dfrn3 3395, and dfrn4 3590.

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 3252	. 2 class ran A
3	1	ccnv 3250	. . 3 class ◡A
4	3	cdm 3251	. 2 class dom ◡ A
5	2, 4	wceq 992	1 wff ran A = dom ◡ A

This definition is referenced by:  dfrn2 3394  dmcnvcnv 3423  rncnvcnv 3424  rneq 3426  rnss 3429  brelrng 3430  rncoss 3451  rncoeq 3454  rnun 3542  rnin 3543  rnxp 3557  rnsnop 3582  op2nda 3584  dfco2a 3599  unidmrn 3621  cnvexg 3624  fncnv 3666  funcnvres 3673  funimacnv 3676  fimacnvdisj 3756  dff1o4 3804  f1ocnv 3809  foimacnv 3814  tz7.48-3 4259  sbthlem5 4596  sbthlem8 4599  sbthlem9 4600  fodomr 4628  inf3lem7 4764  zorn2lem4 4937  fodom 4944  uzrdgvali 6666  cnconst 7990  adj1o 10098  ranncnt 10873  toplat 10884  cvimarndm 11406  ordtypelem4 11430  opncldf1 11454  compfipin0lem 11492  compfipin0 11493  cnvcan 11814  f1ocan1fv 11816

Copyright terms: Public domain