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

Metamath Proof Explorer

Theorem sbcbig

Description: Distribution of class substitution over biconditional. (Contributed by Raph Levien, 10-Apr-2004)

Ref Expression
Assertion sbcbig 
|- ( A e. V -> ( [. A / x ]. ( ph <-> ps ) <-> ( [. A / x ]. ph <-> [. A / x ]. ps ) ) )

Proof

Step Hyp Ref Expression
1 dfsbcq2 
 |-  ( y = A -> ( [ y / x ] ( ph <-> ps ) <-> [. A / x ]. ( ph <-> ps ) ) )
2 dfsbcq2 
 |-  ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
3 dfsbcq2 
 |-  ( y = A -> ( [ y / x ] ps <-> [. A / x ]. ps ) )
4 2 3 bibi12d 
 |-  ( y = A -> ( ( [ y / x ] ph <-> [ y / x ] ps ) <-> ( [. A / x ]. ph <-> [. A / x ]. ps ) ) )
5 sbbi 
 |-  ( [ y / x ] ( ph <-> ps ) <-> ( [ y / x ] ph <-> [ y / x ] ps ) )
6 1 4 5 vtoclbg 
 |-  ( A e. V -> ( [. A / x ]. ( ph <-> ps ) <-> ( [. A / x ]. ph <-> [. A / x ]. ps ) ) )