csbcnv

Description: Move class substitution in and out of the converse of a relation. Version of csbcnvgALT without a sethood antecedent but depending on more axioms. (Contributed by Thierry Arnoux, 8-Feb-2017) (Revised by NM, 23-Aug-2018)

		Ref	Expression
	Assertion	csbcnv	⊢ ^◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ ^◡ 𝐹

Proof

Step	Hyp	Ref	Expression
1		sbcbr	⊢ ( [ 𝐴 / 𝑥 ] 𝑧 𝐹 𝑦 ↔ 𝑧 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 )
2	1	opabbii	⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝑧 𝐹 𝑦 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 }
3		csbopab	⊢ ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 𝐹 𝑦 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝑧 𝐹 𝑦 }
4		df-cnv	⊢ ^◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 }
5	2 3 4	3eqtr4ri	⊢ ^◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 𝐹 𝑦 }
6		df-cnv	⊢ ^◡ 𝐹 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 𝐹 𝑦 }
7	6	csbeq2i	⊢ ⦋ 𝐴 / 𝑥 ⦌ ^◡ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 𝐹 𝑦 }
8	5 7	eqtr4i	⊢ ^◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ ^◡ 𝐹

Metamath Proof Explorer

Theorem csbcnv

Proof