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 = [_ A / x ]_ `' F

Proof

Step Hyp Ref Expression
1 df-cnv 
 |-  `' [_ A / x ]_ F = { <. 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 = { <. y , z >. | [. A / x ]. z F y }
5 csbopabw 
 |-  ( A e. _V -> [_ A / x ]_ { <. y , z >. | z F y } = { <. y , z >. | [. A / x ]. z F y } )
6 4 5 eqtr4id 
 |-  ( A e. _V -> `' [_ A / x ]_ F = [_ A / x ]_ { <. y , z >. | z F y } )
7 df-cnv 
 |-  `' F = { <. y , z >. | z F y }
8 7 csbeq2i 
 |-  [_ A / x ]_ `' F = [_ A / x ]_ { <. y , z >. | z F y }
9 6 8 eqtr4di 
 |-  ( A e. _V -> `' [_ A / x ]_ F = [_ A / x ]_ `' F )
10 cnv0 
 |-  `' (/) = (/)
11 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ F = (/) )
12 11 cnveqd 
 |-  ( -. A e. _V -> `' [_ A / x ]_ F = `' (/) )
13 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ `' F = (/) )
14 10 12 13 3eqtr4a 
 |-  ( -. A e. _V -> `' [_ A / x ]_ F = [_ A / x ]_ `' F )
15 9 14 pm2.61i 
 |-  `' [_ A / x ]_ F = [_ A / x ]_ `' F