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}^{-1}=⦋A/x⦌F^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		df-cnv	$$⊢{⦋A/x⦌F}^{-1}=\left\{⟨y,z⟩|z⦋A/x⦌Fy\right\}$$
2		sbcbr	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}zFy\leftrightarrow z⦋A/x⦌Fy$$
3	2	opabbii	$$⊢\left\{⟨y,z⟩|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}zFy\right\}=\left\{⟨y,z⟩|z⦋A/x⦌Fy\right\}$$
4	1 3	eqtr4i	$$⊢{⦋A/x⦌F}^{-1}=\left\{⟨y,z⟩|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}zFy\right\}$$
5		csbopabw	$$⊢A\in \mathrm{V}\to ⦋A/x⦌\left\{⟨y,z⟩|zFy\right\}=\left\{⟨y,z⟩|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}zFy\right\}$$
6	4 5	eqtr4id	$$⊢A\in \mathrm{V}\to {⦋A/x⦌F}^{-1}=⦋A/x⦌\left\{⟨y,z⟩|zFy\right\}$$
7		df-cnv	$$⊢F^{-1}=\left\{⟨y,z⟩|zFy\right\}$$
8	7	csbeq2i	$$⊢⦋A/x⦌F^{-1}=⦋A/x⦌\left\{⟨y,z⟩|zFy\right\}$$
9	6 8	eqtr4di	$$⊢A\in \mathrm{V}\to {⦋A/x⦌F}^{-1}=⦋A/x⦌F^{-1}$$
10		cnv0	$$⊢{\varnothing }^{-1}=\varnothing$$
11		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F=\varnothing$$
12	11	cnveqd	$$⊢\neg A\in \mathrm{V}\to {⦋A/x⦌F}^{-1}={\varnothing }^{-1}$$
13		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F^{-1}=\varnothing$$
14	10 12 13	3eqtr4a	$$⊢\neg A\in \mathrm{V}\to {⦋A/x⦌F}^{-1}=⦋A/x⦌F^{-1}$$
15	9 14	pm2.61i	$$⊢{⦋A/x⦌F}^{-1}=⦋A/x⦌F^{-1}$$