Theorem sbcalgOLD 3340

Description: Move universal quantifier in and out of class substitution. (Contributed by NM, 16-Jan-2004.) Obsolete as of 17-Aug-2018. Use sbcal 3339 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 3290	. 2 |- ( z = A -> ( [ z / y ] A. x ph <-> [. A / y ]. A. x ph ) )
2		dfsbcq2 3290	. . 3 |- ( z = A -> ( [ z / y ] ph <-> [. A / y ]. ph ) )
3	2	albidv 1680	. 2 |- ( z = A -> ( A. x [ z / y ] ph <-> A. x [. A / y ]. ph ) )
4		sbal 2181	. 2 |- ( [ z / y ] A. x ph <-> A. x [ z / y ] ph )
5	1, 3, 4	vtoclbg 3130	1 |- ( A e. V -> ( [. A / y ]. A. x ph <-> A. x [. A / y ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1368   = wceq 1370   [wsb 1702   e. wcel 1758   [.wsbc 3287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-v 3073  df-sbc 3288

This theorem is referenced by:  sbcssOLD  31552  trsbcVD  31916  sbcssgVD  31922