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

Metamath Proof Explorer

Theorem csbied

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014) (Revised by Mario Carneiro, 13-Oct-2016) Reduce axiom usage. (Revised by GG, 15-Oct-2024)

Ref Expression
Hypotheses csbied.1 
|- ( ph -> A e. V )
csbied.2 
|- ( ( ph /\ x = A ) -> B = C )
Assertion csbied 
|- ( ph -> [_ A / x ]_ B = C )

Proof

Step Hyp Ref Expression
1 csbied.1 
 |-  ( ph -> A e. V )
2 csbied.2 
 |-  ( ( ph /\ x = A ) -> B = C )
3 df-csb 
 |-  [_ A / x ]_ B = { y | [. A / x ]. y e. B }
4 2 eleq2d 
 |-  ( ( ph /\ x = A ) -> ( z e. B <-> z e. C ) )
5 1 4 sbcied 
 |-  ( ph -> ( [. A / x ]. z e. B <-> z e. C ) )
6 5 alrimiv 
 |-  ( ph -> A. z ( [. A / x ]. z e. B <-> z e. C ) )
7 df-clab 
 |-  ( z e. { y | [. A / x ]. y e. B } <-> [ z / y ] [. A / x ]. y e. B )
8 eleq1w 
 |-  ( y = z -> ( y e. B <-> z e. B ) )
9 8 sbcbidv 
 |-  ( y = z -> ( [. A / x ]. y e. B <-> [. A / x ]. z e. B ) )
10 9 sbievw 
 |-  ( [ z / y ] [. A / x ]. y e. B <-> [. A / x ]. z e. B )
11 7 10 bitr2i 
 |-  ( [. A / x ]. z e. B <-> z e. { y | [. A / x ]. y e. B } )
12 11 bibi1i 
 |-  ( ( [. A / x ]. z e. B <-> z e. C ) <-> ( z e. { y | [. A / x ]. y e. B } <-> z e. C ) )
13 12 biimpi 
 |-  ( ( [. A / x ]. z e. B <-> z e. C ) -> ( z e. { y | [. A / x ]. y e. B } <-> z e. C ) )
14 6 13 sylg 
 |-  ( ph -> A. z ( z e. { y | [. A / x ]. y e. B } <-> z e. C ) )
15 dfcleq 
 |-  ( { y | [. A / x ]. y e. B } = C <-> A. z ( z e. { y | [. A / x ]. y e. B } <-> z e. C ) )
16 14 15 sylibr 
 |-  ( ph -> { y | [. A / x ]. y e. B } = C )
17 3 16 eqtrid 
 |-  ( ph -> [_ A / x ]_ B = C )