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 𝐴 = Fix ◡ 𝐴

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1 1	brcnv	⊢ ( 𝑥 ◡ 𝐴 𝑥 ↔ 𝑥 𝐴 𝑥 )
3	1	elfix	⊢ ( 𝑥 ∈ Fix ◡ 𝐴 ↔ 𝑥 ◡ 𝐴 𝑥 )
4	1	elfix	⊢ ( 𝑥 ∈ Fix 𝐴 ↔ 𝑥 𝐴 𝑥 )
5	2 3 4	3bitr4ri	⊢ ( 𝑥 ∈ Fix 𝐴 ↔ 𝑥 ∈ Fix ◡ 𝐴 )
6	5	eqriv	⊢ Fix 𝐴 = Fix ◡ 𝐴