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	$⊢ 𝖥𝗂𝗑 A = 𝖥𝗂𝗑 A^{-1}$

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2	1 1	brcnv	$⊢ x A^{-1} x \leftrightarrow x A x$
3	1	elfix	$⊢ x \in 𝖥𝗂𝗑 A^{-1} \leftrightarrow x A^{-1} x$
4	1	elfix	$⊢ x \in 𝖥𝗂𝗑 A \leftrightarrow x A x$
5	2 3 4	3bitr4ri	$⊢ x \in 𝖥𝗂𝗑 A \leftrightarrow x \in 𝖥𝗂𝗑 A^{-1}$
6	5	eqriv	$⊢ 𝖥𝗂𝗑 A = 𝖥𝗂𝗑 A^{-1}$