Theorem sbalyz 1872

Description: Move universal quantifier in and out of substitution. Identical to sbal 1873 except that it has an additional distinct variable constraint on y and z. (Contributed by Jim Kingdon, 29-Dec-2017.)

Assertion

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

Distinct variable group:   x,y,z

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

Proof of Theorem sbalyz

Step	Hyp	Ref	Expression
1		nfa1 1431	. . . 4 |- F/xA.xph
2	1	nfsbxy 1815	. . 3 |- F/x[z / y]A.xph
3		ax-4 1397	. . . 4 |- (A.xph -> ph)
4	3	sbimi 1644	. . 3 |- ([z / y]A.xph -> [z / y]ph)
5	2, 4	alrimi 1412	. 2 |- ([z / y]A.xph -> A.x[z / y]ph)
6		sb6 1763	. . . . 5 |- ([z / y]ph <-> A.y(y = z -> ph))
7	6	albii 1356	. . . 4 |- (A.x[z / y]ph <-> A.xA.y(y = z -> ph))
8		alcom 1364	. . . 4 |- (A.xA.y(y = z -> ph) <-> A.yA.x(y = z -> ph))
9	7, 8	bitri 173	. . 3 |- (A.x[z / y]ph <-> A.yA.x(y = z -> ph))
10		nfv 1418	. . . . . 6 |- F/x y = z
11	10	stdpc5 1473	. . . . 5 |- (A.x(y = z -> ph) -> (y = z -> A.xph))
12	11	alimi 1341	. . . 4 |- (A.yA.x(y = z -> ph) -> A.y(y = z -> A.xph))
13		sb2 1647	. . . 4 |- (A.y(y = z -> A.xph) -> [z / y]A.xph)
14	12, 13	syl 14	. . 3 |- (A.yA.x(y = z -> ph) -> [z / y]A.xph)
15	9, 14	sylbi 114	. 2 |- (A.x[z / y]ph -> [z / y]A.xph)
16	5, 15	impbii 117	1 |- ([z / y]A.xph <-> A.x[z / y]ph)

Syntax hints:   -> wi 4   <-> wb 98  A.wal 1240  [wsb 1642

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643

This theorem is referenced by:  sbal  1873