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 = [_ A / x ]_ `' F

Proof

Step	Hyp	Ref	Expression
1		sbcbr	|- ( [. A / x ]. z F y <-> z [_ A / x ]_ F y )
2	1	opabbii	|- { <. y , z >. | [. A / x ]. z F y } = { <. y , z >. | z [_ A / x ]_ F y }
3		csbopab	|- [_ A / x ]_ { <. y , z >. | z F y } = { <. y , z >. | [. A / x ]. z F y }
4		df-cnv	|- `' [_ A / x ]_ F = { <. y , z >. | z [_ A / x ]_ F y }
5	2 3 4	3eqtr4ri	|- `' [_ A / x ]_ F = [_ A / x ]_ { <. y , z >. | z F y }
6		df-cnv	|- `' F = { <. y , z >. | z F y }
7	6	csbeq2i	|- [_ A / x ]_ `' F = [_ A / x ]_ { <. y , z >. | z F y }
8	5 7	eqtr4i	|- `' [_ A / x ]_ F = [_ A / x ]_ `' F