This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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