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 ) ) )