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	⊢ ( 𝐴 ∈ 𝑉 → ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		sbcbr123	⊢ ( [ 𝐴 / 𝑥 ] 𝑧 𝐹 𝑦 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝑦 )
2		csbconstg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑧 = 𝑧 )
3		csbconstg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 )
4	2 3	breq12d	⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ↔ 𝑧 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 ) )
5	1 4	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 𝐹 𝑦 ↔ 𝑧 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 ) )
6	5	opabbidv	⊢ ( 𝐴 ∈ 𝑉 → { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝑧 𝐹 𝑦 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 } )
7		csbopabgALT	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 𝐹 𝑦 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝑧 𝐹 𝑦 } )
8		df-cnv	⊢ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 }
9	8	a1i	⊢ ( 𝐴 ∈ 𝑉 → ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 } )
10	6 7 9	3eqtr4rd	⊢ ( 𝐴 ∈ 𝑉 → ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 𝐹 𝑦 } )
11		df-cnv	⊢ ◡ 𝐹 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 𝐹 𝑦 }
12	11	csbeq2i	⊢ ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 𝐹 𝑦 }
13	10 12	eqtr4di	⊢ ( 𝐴 ∈ 𝑉 → ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝐹 )