Theorem sbcalgOLD 36946

Description: Move universal quantifier in and out of class substitution. (Contributed by NM, 16-Jan-2004.) Obsolete as of 17-Aug-2018. Use sbcal 3328 instead. (New usage is discouraged.) (Proof modification is discouraged.)

Assertion

Ref	Expression
sbcalgOLD	|- ( A e. V -> ( [. A / y ]. A. x ph <-> A. x [. A / y ]. ph ) )

Distinct variable groups:   x, A   x, y

Allowed substitution hints:   ph( x, y)   A( y)   V( x, y)

Proof of Theorem sbcalgOLD

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsbcq2 3281	. 2 |- ( z = A -> ( [ z / y ] A. x ph <-> [. A / y ]. A. x ph ) )
2		dfsbcq2 3281	. . 3 |- ( z = A -> ( [ z / y ] ph <-> [. A / y ]. ph ) )
3	2	albidv 1777	. 2 |- ( z = A -> ( A. x [ z / y ] ph <-> A. x [. A / y ]. ph ) )
4		sbal 2301	. 2 |- ( [ z / y ] A. x ph <-> A. x [ z / y ] ph )
5	1, 3, 4	vtoclbg 3119	1 |- ( A e. V -> ( [. A / y ]. A. x ph <-> A. x [. A / y ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 189   A.wal 1452   = 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-11 1930  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:  sbcssOLD  36950  trsbcVD  37313  sbcssgVD  37319