This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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