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

Proof

Step Hyp Ref Expression
1 sbcbr123 ⊢ [˙A / x]˙ z F y ↔ ⦋ A / x⦌ z ⦋ A / x⦌ F ⦋ A / x⦌ y
2 csbconstg ⊢ A ∈ V → ⦋ A / x⦌ z = z
3 csbconstg ⊢ A ∈ V → ⦋ A / x⦌ y = y
4 2 3 breq12d ⊢ A ∈ V → ⦋ A / x⦌ z ⦋ A / x⦌ F ⦋ A / x⦌ y ↔ z ⦋ A / x⦌ F y
5 1 4 bitrid ⊢ A ∈ V → [˙A / x]˙ z F y ↔ z ⦋ A / x⦌ F y
6 5 opabbidv ⊢ A ∈ V → y z | [˙A / x]˙ z F y = y z | z ⦋ A / x⦌ F y
7 csbopabgALT ⊢ A ∈ V → ⦋ A / x⦌ y z | z F y = y z | [˙A / x]˙ z F y
8 df-cnv ⊢ ⦋ A / x⦌ F -1 = y z | z ⦋ A / x⦌ F y
9 8 a1i ⊢ A ∈ V → ⦋ A / x⦌ F -1 = y z | z ⦋ A / x⦌ F y
10 6 7 9 3eqtr4rd ⊢ A ∈ V → ⦋ A / x⦌ F -1 = ⦋ A / x⦌ y z | z F y
11 df-cnv ⊢ F -1 = y z | z F y
12 11 csbeq2i ⊢ ⦋ A / x⦌ F -1 = ⦋ A / x⦌ y z | z F y
13 10 12 eqtr4di ⊢ A ∈ V → ⦋ A / x⦌ F -1 = ⦋ A / x⦌ F -1