Definition df-rn 4138

Description: Define the range of a class. For an alternate definitions, see dfrn2 4275, dfrn3 4276, and dfrn4 4487. The notation "ran " is used by Enderton; other authors sometimes use script R or script W.

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 4120	. 2 class ran A
3	1	ccnv 4118	. . 3 class `'A
4	3	cdm 4119	. 2 class dom `' A
5	2, 4	wceq 1586	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2 4275  dmcnvcnv 4304  rncnvcnv 4305  rneq 4307  rnss 4310  brelrng 4311  rncoss 4334  rncoeq 4337  cvimarndm 4405  rnun 4434  rnin 4435  rnxp 4449  rnxpss 4451  rnsnop 4479  unidmrn 4523  dfdm2 4524  cnvexg 4527  fncnv 4580  funcnvres 4587  funimacnv 4590  fimacnvdisj 4681  dff1o4 4730  foimacnv 4740  tz7.48-3 5332  sbthlem5 5680  sbthlem8 5683  sbthlem9 5684  fodomr 5716  ordtypelem4 5918  inf3lem7OLD 5958  zorn2lem4 6364  fodom 6374  uzrdgvali 8085  cnconst 9923  adj1o 12287  fldcnv 15069  rnintintrn 15199  domcnvpre 15313  ranncnt 15364  toplat 15377  ordtypelem4OLD 16202  opncldf1 16226  compfipin0lem 16259  compfipin0 16260  cnvcan 16539  f1ocan1fv 16541

Copyright terms: Public domain