Theorem csbcnvgALT

Description: Move class substitution in and out of the converse of a relation. Version of csbcnv with a sethood antecedent but depending on fewer axioms. (Contributed by Thierry Arnoux, 8-Feb-2017) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	csbcnvgALT	|- ( A e. V -> `' [_ A / x ]_ F = [_ A / x ]_ `' F )

Proof

Step	Hyp	Ref	Expression
1		sbcbr123	|- ( [. A / x ]. z F y <-> [_ A / x ]_ z [_ A / x ]_ F [_ A / x ]_ y )
2		csbconstg	|- ( A e. V -> [_ A / x ]_ z = z )
3		csbconstg	|- ( A e. V -> [_ A / x ]_ y = y )
4	2 3	breq12d	|- ( A e. V -> ( [_ A / x ]_ z [_ A / x ]_ F [_ A / x ]_ y <-> z [_ A / x ]_ F y ) )
5	1 4	bitrid	|- ( A e. V -> ( [. A / x ]. z F y <-> z [_ A / x ]_ F y ) )
6	5	opabbidv	|- ( A e. V -> { <. y , z >. | [. A / x ]. z F y } = { <. y , z >. | z [_ A / x ]_ F y } )
7		csbopabgALT	|- ( A e. V -> [_ A / x ]_ { <. y , z >. | z F y } = { <. y , z >. | [. A / x ]. z F y } )
8		df-cnv	|- `' [_ A / x ]_ F = { <. y , z >. | z [_ A / x ]_ F y }
9	8	a1i	|- ( A e. V -> `' [_ A / x ]_ F = { <. y , z >. | z [_ A / x ]_ F y } )
10	6 7 9	3eqtr4rd	|- ( A e. V -> `' [_ A / x ]_ F = [_ A / x ]_ { <. y , z >. | z F y } )
11		df-cnv	|- `' F = { <. y , z >. | z F y }
12	11	csbeq2i	|- [_ A / x ]_ `' F = [_ A / x ]_ { <. y , z >. | z F y }
13	10 12	eqtr4di	|- ( A e. V -> `' [_ A / x ]_ F = [_ A / x ]_ `' F )