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

Proof

Step	Hyp	Ref	Expression
1		sbcbr123	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}zFy\leftrightarrow ⦋A/x⦌z⦋A/x⦌F⦋A/x⦌y$$
2		csbconstg	$$⊢A\in V\to ⦋A/x⦌z=z$$
3		csbconstg	$$⊢A\in V\to ⦋A/x⦌y=y$$
4	2 3	breq12d	$$⊢A\in V\to \left(⦋A/x⦌z⦋A/x⦌F⦋A/x⦌y\leftrightarrow z⦋A/x⦌Fy\right)$$
5	1 4	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}zFy\leftrightarrow z⦋A/x⦌Fy\right)$$
6	5	opabbidv	$$⊢A\in V\to \left\{⟨y,z⟩|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}zFy\right\}=\left\{⟨y,z⟩|z⦋A/x⦌Fy\right\}$$
7		csbopabgALT	$$⊢A\in V\to ⦋A/x⦌\left\{⟨y,z⟩|zFy\right\}=\left\{⟨y,z⟩|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}zFy\right\}$$
8		df-cnv	$$⊢{⦋A/x⦌F}^{-1}=\left\{⟨y,z⟩|z⦋A/x⦌Fy\right\}$$
9	8	a1i	$$⊢A\in V\to {⦋A/x⦌F}^{-1}=\left\{⟨y,z⟩|z⦋A/x⦌Fy\right\}$$
10	6 7 9	3eqtr4rd	$$⊢A\in V\to {⦋A/x⦌F}^{-1}=⦋A/x⦌\left\{⟨y,z⟩|zFy\right\}$$
11		df-cnv	$$⊢F^{-1}=\left\{⟨y,z⟩|zFy\right\}$$
12	11	csbeq2i	$$⊢⦋A/x⦌F^{-1}=⦋A/x⦌\left\{⟨y,z⟩|zFy\right\}$$
13	10 12	eqtr4di	$$⊢A\in V\to {⦋A/x⦌F}^{-1}=⦋A/x⦌F^{-1}$$