Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Preparatory theorems
rncnv
Next ⟩
dfdm6
Metamath Proof Explorer
Ascii
Unicode
Theorem
rncnv
Description:
Range of converse is the domain.
(Contributed by
Peter Mazsa
, 12-Feb-2018)
Ref
Expression
Assertion
rncnv
⊢
ran
⁡
A
-1
=
dom
⁡
A
Proof
Step
Hyp
Ref
Expression
1
dfdm4
⊢
dom
⁡
A
=
ran
⁡
A
-1
2
1
eqcomi
⊢
ran
⁡
A
-1
=
dom
⁡
A