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

Metamath Proof Explorer

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