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

Metamath Proof Explorer

Theorem csbab

Description: Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005) (Revised by NM, 19-Aug-2018)

Ref Expression
Assertion csbab 
|- [_ A / x ]_ { y | ph } = { y | [. A / x ]. ph }

Proof

Step Hyp Ref Expression
1 df-clab 
 |-  ( z e. { y | [. A / x ]. ph } <-> [ z / y ] [. A / x ]. ph )
2 sbsbc 
 |-  ( [ z / y ] [. A / x ]. ph <-> [. z / y ]. [. A / x ]. ph )
3 1 2 bitri 
 |-  ( z e. { y | [. A / x ]. ph } <-> [. z / y ]. [. A / x ]. ph )
4 sbccom 
 |-  ( [. z / y ]. [. A / x ]. ph <-> [. A / x ]. [. z / y ]. ph )
5 df-clab 
 |-  ( z e. { y | ph } <-> [ z / y ] ph )
6 sbsbc 
 |-  ( [ z / y ] ph <-> [. z / y ]. ph )
7 5 6 bitri 
 |-  ( z e. { y | ph } <-> [. z / y ]. ph )
8 7 sbcbii 
 |-  ( [. A / x ]. z e. { y | ph } <-> [. A / x ]. [. z / y ]. ph )
9 4 8 bitr4i 
 |-  ( [. z / y ]. [. A / x ]. ph <-> [. A / x ]. z e. { y | ph } )
10 sbcel2 
 |-  ( [. A / x ]. z e. { y | ph } <-> z e. [_ A / x ]_ { y | ph } )
11 3 9 10 3bitrri 
 |-  ( z e. [_ A / x ]_ { y | ph } <-> z e. { y | [. A / x ]. ph } )
12 11 eqriv 
 |-  [_ A / x ]_ { y | ph } = { y | [. A / x ]. ph }