Theorem csbcnv

Description: Move class substitution in and out of the converse of a relation. (Contributed by Thierry Arnoux, 8-Feb-2017) (Revised by NM, 23-Aug-2018) Remove dependency on ax-sep and ax-pr . (Revised by Eric Schmidt, 4-Jun-2026)

	Ref	Expression
Assertion	csbcnv	|- `' [_ A / x ]_ F = [_ A / x ]_ `' F

Proof

Step	Hyp	Ref	Expression
1		df-cnv	|- `' [_ A / x ]_ F = { <. y , z >. | z [_ A / x ]_ F y }
2		sbcbr	|- ( [. A / x ]. z F y <-> z [_ A / x ]_ F y )
3	2	opabbii	|- { <. y , z >. | [. A / x ]. z F y } = { <. y , z >. | z [_ A / x ]_ F y }
4	1 3	eqtr4i	|- `' [_ A / x ]_ F = { <. y , z >. | [. A / x ]. z F y }
5		csbopabw	|- ( A e. _V -> [_ A / x ]_ { <. y , z >. | z F y } = { <. y , z >. | [. A / x ]. z F y } )
6	4 5	eqtr4id	|- ( A e. _V -> `' [_ A / x ]_ F = [_ A / x ]_ { <. y , z >. | z F y } )
7		df-cnv	|- `' F = { <. y , z >. | z F y }
8	7	csbeq2i	|- [_ A / x ]_ `' F = [_ A / x ]_ { <. y , z >. | z F y }
9	6 8	eqtr4di	|- ( A e. _V -> `' [_ A / x ]_ F = [_ A / x ]_ `' F )
10		cnv0	|- `' (/) = (/)
11		csbprc	|- ( -. A e. _V -> [_ A / x ]_ F = (/) )
12	11	cnveqd	|- ( -. A e. _V -> `' [_ A / x ]_ F = `' (/) )
13		csbprc	|- ( -. A e. _V -> [_ A / x ]_ `' F = (/) )
14	10 12 13	3eqtr4a	|- ( -. A e. _V -> `' [_ A / x ]_ F = [_ A / x ]_ `' F )
15	9 14	pm2.61i	|- `' [_ A / x ]_ F = [_ A / x ]_ `' F