Theorem csbcnv

Description: Move class substitution in and out of the converse of a relation. Version of csbcnvgALT without a sethood antecedent but depending on more axioms. (Contributed by Thierry Arnoux, 8-Feb-2017) (Revised by NM, 23-Aug-2018)

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

Proof

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