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

Metamath Proof Explorer

Theorem sbcied

Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014) Avoid ax-10 , ax-12 . (Revised by GG, 12-Oct-2024)

Ref Expression
Hypotheses sbcied.1 
|- ( ph -> A e. V )
sbcied.2 
|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
Assertion sbcied 
|- ( ph -> ( [. A / x ]. ps <-> ch ) )

Proof

Step Hyp Ref Expression
1 sbcied.1 
 |-  ( ph -> A e. V )
2 sbcied.2 
 |-  ( ( ph /\ x = A ) -> ( ps <-> ch ) )
3 df-sbc 
 |-  ( [. A / x ]. ps <-> A e. { x | ps } )
4 1 2 elabd3 
 |-  ( ph -> ( A e. { x | ps } <-> ch ) )
5 3 4 bitrid 
 |-  ( ph -> ( [. A / x ]. ps <-> ch ) )