Description: The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007) Do not depend on cnvcnv in order to prove it from cnvcnv2 . (Revised by BJ, 16-Oct-2026) Do not depend on cnvcnv . (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-cnvcnv2 | |- `' `' A = ( A |` _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnvcnv3 | |- `' `' A = { <. x , y >. | x A y } |
|
| 2 | relpart | |- ( A |` _V ) = { <. x , y >. | x A y } |
|
| 3 | 1 2 | eqtr4i | |- `' `' A = ( A |` _V ) |