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	⊢ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝐹

Proof

Step	Hyp	Ref	Expression
1		df-cnv	⊢ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 }
2		sbcbr	⊢ ( [ 𝐴 / 𝑥 ] 𝑧 𝐹 𝑦 ↔ 𝑧 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 )
3	2	opabbii	⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝑧 𝐹 𝑦 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑦 }
4	1 3	eqtr4i	⊢ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝑧 𝐹 𝑦 }
5		csbopabw	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 𝐹 𝑦 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝑧 𝐹 𝑦 } )
6	4 5	eqtr4id	⊢ ( 𝐴 ∈ V → ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 𝐹 𝑦 } )
7		df-cnv	⊢ ◡ 𝐹 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 𝐹 𝑦 }
8	7	csbeq2i	⊢ ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑧 𝐹 𝑦 }
9	6 8	eqtr4di	⊢ ( 𝐴 ∈ V → ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝐹 )
10		cnv0	⊢ ◡ ∅ = ∅
11		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ∅ )
12	11	cnveqd	⊢ ( ¬ 𝐴 ∈ V → ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ◡ ∅ )
13		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝐹 = ∅ )
14	10 12 13	3eqtr4a	⊢ ( ¬ 𝐴 ∈ V → ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝐹 )
15	9 14	pm2.61i	⊢ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝐹