Theorem sbcangOLD 36933

Description: Distribution of class substitution over conjunction. (Contributed by NM, 21-May-2004.) Obsolete as of 17-Aug-2018. Use sbcan 3321 instead. (New usage is discouraged.) (Proof modification is discouraged.)

Assertion

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

Proof of Theorem sbcangOLD

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsbcq2 3281	. 2 |- ( y = A -> ( [ y / x ] ( ph /\ ps ) <-> [. A / x ]. ( ph /\ ps ) ) )
2		dfsbcq2 3281	. . 3 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
3		dfsbcq2 3281	. . 3 |- ( y = A -> ( [ y / x ] ps <-> [. A / x ]. ps ) )
4	2, 3	anbi12d 722	. 2 |- ( y = A -> ( ( [ y / x ] ph /\ [ y / x ] ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) ) )
5		sban 2238	. 2 |- ( [ y / x ] ( ph /\ ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )
6	1, 4, 5	vtoclbg 3119	1 |- ( A e. V -> ( [. A / x ]. ( ph /\ ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1454   [wsb 1807   e. wcel 1897   [.wsbc 3278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-v 3058  df-sbc 3279

This theorem is referenced by:  csbunigOLD  37251  csbxpgOLD  37253  csbingVD  37320  onfrALTlem5VD  37321  onfrALTlem4VD  37322  csbxpgVD  37330  csbunigVD  37334