Metamath Proof Explorer

Theorem fixcnv

Description: The fixpoints of a class are the same as those of its converse. (Contributed by Scott Fenton, 16-Apr-2012)

Ref Expression
Assertion fixcnv 
|- Fix A = Fix `' A

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 1 brcnv 
 |-  ( x `' A x <-> x A x )
3 1 elfix 
 |-  ( x e. Fix `' A <-> x `' A x )
4 1 elfix 
 |-  ( x e. Fix A <-> x A x )
5 2 3 4 3bitr4ri 
 |-  ( x e. Fix A <-> x e. Fix `' A )
6 5 eqriv 
 |-  Fix A = Fix `' A