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 ⊢ ⦋ A / x⦌ F -1 = ⦋ A / x⦌ F -1

Proof

Step Hyp Ref Expression
1 df-cnv ⊢ ⦋ A / x⦌ F -1 = y z | z ⦋ A / x⦌ F y
2 sbcbr ⊢ [˙A / x]˙ z F y ↔ z ⦋ A / x⦌ F y
3 2 opabbii ⊢ y z | [˙A / x]˙ z F y = y z | z ⦋ A / x⦌ F y
4 1 3 eqtr4i ⊢ ⦋ A / x⦌ F -1 = y z | [˙A / x]˙ z F y
5 csbopabw ⊢ A ∈ V → ⦋ A / x⦌ y z | z F y = y z | [˙A / x]˙ z F y
6 4 5 eqtr4id ⊢ A ∈ V → ⦋ A / x⦌ F -1 = ⦋ A / x⦌ y z | z F y
7 df-cnv ⊢ F -1 = y z | z F y
8 7 csbeq2i ⊢ ⦋ A / x⦌ F -1 = ⦋ A / x⦌ y z | z F y
9 6 8 eqtr4di ⊢ A ∈ V → ⦋ A / x⦌ F -1 = ⦋ A / x⦌ F -1
10 cnv0 ⊢ ∅ -1 = ∅
11 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ F = ∅
12 11 cnveqd ⊢ ¬ A ∈ V → ⦋ A / x⦌ F -1 = ∅ -1
13 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ F -1 = ∅
14 10 12 13 3eqtr4a ⊢ ¬ A ∈ V → ⦋ A / x⦌ F -1 = ⦋ A / x⦌ F -1
15 9 14 pm2.61i ⊢ ⦋ A / x⦌ F -1 = ⦋ A / x⦌ F -1