Definition df-rn 3179

Description: Define the range of a class. For an alternate definitions, see dfrn2 3292, dfrn3 3293, and dfrn4 3478.

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 3161	. 2 class ran A
3	1	ccnv 3159	. . 3 class `'A
4	3	cdm 3160	. 2 class dom `' A
5	2, 4	wceq 953	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2 3292  dmcnvcnv 3325  rncnvcnv 3326  rneq 3328  rnss 3331  brelrn 3332  rncoss 3348  rncoeq 3351  rnsnop 3436  op2nda 3438  rnun 3443  rnin 3444  rnxp 3458  cnvexg 3505  fncnv 3547  funcnvres 3554  funimacnv 3557  fimacnvdisj 3634  f1o4 3681  f1ocnv 3686  tz7.48-3 3943  sbthlem5 4431  sbthlem8 4434  sbthlem9 4435  fodomr 4463  inf3lem7 4591  zorn2lem4 4763  fodom 4770  uzrdgval 6239  cnconst 7719  adj1o 9735

Copyright terms: Public domain