Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Relations
cnvcnvres
Next ⟩
imacnvcnv
Metamath Proof Explorer
Ascii
Unicode
Theorem
cnvcnvres
Description:
The double converse of the restriction of a class.
(Contributed by
NM
, 3-Jun-2007)
Ref
Expression
Assertion
cnvcnvres
⊢
A
↾
B
-1
-1
=
A
-1
-1
↾
B
Proof
Step
Hyp
Ref
Expression
1
relres
⊢
Rel
⁡
A
↾
B
2
dfrel2
⊢
Rel
⁡
A
↾
B
↔
A
↾
B
-1
-1
=
A
↾
B
3
1
2
mpbi
⊢
A
↾
B
-1
-1
=
A
↾
B
4
rescnvcnv
⊢
A
-1
-1
↾
B
=
A
↾
B
5
3
4
eqtr4i
⊢
A
↾
B
-1
-1
=
A
-1
-1
↾
B