Theorem nfsbxyt 1816

Description: Closed form of nfsbxy 1815. (Contributed by Jim Kingdon, 9-May-2018.)

Assertion

Ref	Expression
nfsbxyt	|- (A.x F/zph -> F/z[y / x]ph)

Distinct variable groups:   x,y   y,z

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

Proof of Theorem nfsbxyt

Step	Hyp	Ref	Expression
1		ax-bnd 1396	. 2 |- (A.z z = x \/ (A.z z = y \/ A.xA.z(x = y -> A.z x = y)))
2		nfs1v 1812	. . . . 5 |- F/z[y / z]ph
3		drsb1 1677	. . . . . 6 |- (A.z z = x -> ([y / z]ph <-> [y / x]ph))
4	3	drnf2 1619	. . . . 5 |- (A.z z = x -> ( F/z[y / z]ph <-> F/z[y / x]ph))
5	2, 4	mpbii 136	. . . 4 |- (A.z z = x -> F/z[y / x]ph)
6	5	a1d 22	. . 3 |- (A.z z = x -> (A.x F/zph -> F/z[y / x]ph))
7		a16nf 1743	. . . . 5 |- (A.z z = y -> F/z[y / x]ph)
8	7	a1d 22	. . . 4 |- (A.z z = y -> (A.x F/zph -> F/z[y / x]ph))
9		df-nf 1347	. . . . . 6 |- ( F/z x = y <-> A.z(x = y -> A.z x = y))
10	9	albii 1356	. . . . 5 |- (A.x F/z x = y <-> A.xA.z(x = y -> A.z x = y))
11		sb5 1764	. . . . . . 7 |- ([y / x]ph <-> E.x(x = y /\ ph))
12		nfa1 1431	. . . . . . . . 9 |- F/xA.x F/z x = y
13		nfa1 1431	. . . . . . . . 9 |- F/xA.x F/zph
14	12, 13	nfan 1454	. . . . . . . 8 |- F/x(A.x F/z x = y /\ A.x F/zph)
15		sp 1398	. . . . . . . . . 10 |- (A.x F/z x = y -> F/z x = y)
16	15	adantr 261	. . . . . . . . 9 |- ((A.x F/z x = y /\ A.x F/zph) -> F/z x = y)
17		sp 1398	. . . . . . . . . 10 |- (A.x F/zph -> F/zph)
18	17	adantl 262	. . . . . . . . 9 |- ((A.x F/z x = y /\ A.x F/zph) -> F/zph)
19	16, 18	nfand 1457	. . . . . . . 8 |- ((A.x F/z x = y /\ A.x F/zph) -> F/z(x = y /\ ph))
20	14, 19	nfexd 1641	. . . . . . 7 |- ((A.x F/z x = y /\ A.x F/zph) -> F/zE.x(x = y /\ ph))
21	11, 20	nfxfrd 1361	. . . . . 6 |- ((A.x F/z x = y /\ A.x F/zph) -> F/z[y / x]ph)
22	21	ex 108	. . . . 5 |- (A.x F/z x = y -> (A.x F/zph -> F/z[y / x]ph))
23	10, 22	sylbir 125	. . . 4 |- (A.xA.z(x = y -> A.z x = y) -> (A.x F/zph -> F/z[y / x]ph))
24	8, 23	jaoi 635	. . 3 |- ((A.z z = y \/ A.xA.z(x = y -> A.z x = y)) -> (A.x F/zph -> F/z[y / x]ph))
25	6, 24	jaoi 635	. 2 |- ((A.z z = x \/ (A.z z = y \/ A.xA.z(x = y -> A.z x = y))) -> (A.x F/zph -> F/z[y / x]ph))
26	1, 25	ax-mp 7	1 |- (A.x F/zph -> F/z[y / x]ph)

Syntax hints:   -> wi 4   /\ wa 97   \/ wo 628  A.wal 1240   F/wnf 1346  E.wex 1378  [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

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

This theorem is referenced by:  nfsbt  1847