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

Metamath Proof Explorer

Theorem csbcnvOLD

Description: Obsolete version of csbcnv as of 4-Jun-2026. (Contributed by Thierry Arnoux, 8-Feb-2017) (Revised by NM, 23-Aug-2018) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	csbcnvOLD	$⊢ {⦋ A / x ⦌ F}^{-1} = ⦋ A / x ⦌ F^{-1}$

Proof

Step	Hyp	Ref	Expression
1		sbcbr	$⊢ \underset{˙}{[} A / x \underset{˙}{]} z F y \leftrightarrow z ⦋ A / x ⦌ F y$
2	1	opabbii	$⊢ \{⟨y, z⟩ \| \underset{˙}{[} A / x \underset{˙}{]} z F y\} = \{⟨y, z⟩ \| z ⦋ A / x ⦌ F y\}$
3		csbopab	$⊢ ⦋ A / x ⦌ \{⟨y, z⟩ \| z F y\} = \{⟨y, z⟩ \| \underset{˙}{[} A / x \underset{˙}{]} z F y\}$
4		df-cnv	$⊢ {⦋ A / x ⦌ F}^{-1} = \{⟨y, z⟩ \| z ⦋ A / x ⦌ F y\}$
5	2 3 4	3eqtr4ri	$⊢ {⦋ A / x ⦌ F}^{-1} = ⦋ A / x ⦌ \{⟨y, z⟩ \| z F y\}$
6		df-cnv	$⊢ F^{-1} = \{⟨y, z⟩ \| z F y\}$
7	6	csbeq2i	$⊢ ⦋ A / x ⦌ F^{-1} = ⦋ A / x ⦌ \{⟨y, z⟩ \| z F y\}$
8	5 7	eqtr4i	$⊢ {⦋ A / x ⦌ F}^{-1} = ⦋ A / x ⦌ F^{-1}$