| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define the range of a class. For an alternate definitions, see dfrn2 3292, dfrn3 3293, and dfrn4 3478. |
| Ref | Expression |
|---|---|
| df-rn |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . 3
| |
| 2 | 1 | crn 3161 |
. 2
|
| 3 | 1 | ccnv 3159 |
. . 3
|
| 4 | 3 | cdm 3160 |
. 2
|
| 5 | 2, 4 | wceq 953 |
1
|
| Colors of variables: wff set class |
| 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 |