Theorem sbcalf 33917

Description: Move universal quantifier in and out of class substitution, with an explicit non-free variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.)

Hypothesis

Ref	Expression
sbcalf.1	|- F/_ y A

Assertion

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

Distinct variable group:   x, y

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

Proof of Theorem sbcalf

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1843	. . . 4 |- F/ z ph
2	1	sb8 2424	. . 3 |- ( A. y ph <-> A. z [ z / y ] ph )
3	2	sbcbii 3491	. 2 |- ( [. A / x ]. A. y ph <-> [. A / x ]. A. z [ z / y ] ph )
4		sbcal 3485	. 2 |- ( [. A / x ]. A. z [ z / y ] ph <-> A. z [. A / x ]. [ z / y ] ph )
5		sbcalf.1	. . . 4 |- F/_ y A
6		nfs1v 2437	. . . 4 |- F/ y [ z / y ] ph
7	5, 6	nfsbc 3457	. . 3 |- F/ y [. A / x ]. [ z / y ] ph
8		nfv 1843	. . 3 |- F/ z [. A / x ]. ph
9		sbequ12r 2112	. . . 4 |- ( z = y -> ( [ z / y ] ph <-> ph ) )
10	9	sbcbidv 3490	. . 3 |- ( z = y -> ( [. A / x ]. [ z / y ] ph <-> [. A / x ]. ph ) )
11	7, 8, 10	cbval 2271	. 2 |- ( A. z [. A / x ]. [ z / y ] ph <-> A. y [. A / x ]. ph )
12	3, 4, 11	3bitri 286	1 |- ( [. A / x ]. A. y ph <-> A. y [. A / x ]. ph )

Syntax hints:   <-> wb 196   A.wal 1481   [wsb 1880   F/_wnfc 2751   [.wsbc 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sbc 3436

This theorem is referenced by:  sbcalfi  33919