Theorem sbcnestgf 3184

Description: Nest the composition of two substitutions. (Contributed by Mario Carneiro, 11-Nov-2016.)

Assertion

Ref	Expression
sbcnestgf	|- ((A e. V /\ A.y F/xph) -> ( [.A / x ]. [.B / y ].ph <-> [.[_A / x]_B / y ].ph))

Proof of Theorem sbcnestgf

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsbcq 3049	. . . . 5 |- (z = A -> ( [.z / x ]. [.B / y ].ph <-> [.A / x ]. [.B / y ].ph))
2		csbeq1 3140	. . . . . 6 |- (z = A -> [_z / x]_B = [_A / x]_B)
3		dfsbcq 3049	. . . . . 6 |- ([_z / x]_B = [_A / x]_B -> ( [.[_z / x]_B / y ].ph <-> [.[_A / x]_B / y ].ph))
4	2, 3	syl 15	. . . . 5 |- (z = A -> ( [.[_z / x]_B / y ].ph <-> [.[_A / x]_B / y ].ph))
5	1, 4	bibi12d 312	. . . 4 |- (z = A -> (( [.z / x ]. [.B / y ].ph <-> [.[_z / x]_B / y ].ph) <-> ( [.A / x ]. [.B / y ].ph <-> [.[_A / x]_B / y ].ph)))
6	5	imbi2d 307	. . 3 |- (z = A -> ((A.y F/xph -> ( [.z / x ]. [.B / y ].ph <-> [.[_z / x]_B / y ].ph)) <-> (A.y F/xph -> ( [.A / x ]. [.B / y ].ph <-> [.[_A / x]_B / y ].ph))))
7		vex 2863	. . . . 5 |- z e. _V
8	7	a1i 10	. . . 4 |- (A.y F/xph -> z e. _V)
9		csbeq1a 3145	. . . . . 6 |- (x = z -> B = [_z / x]_B)
10		dfsbcq 3049	. . . . . 6 |- (B = [_z / x]_B -> ( [.B / y ].ph <-> [.[_z / x]_B / y ].ph))
11	9, 10	syl 15	. . . . 5 |- (x = z -> ( [.B / y ].ph <-> [.[_z / x]_B / y ].ph))
12	11	adantl 452	. . . 4 |- ((A.y F/xph /\ x = z) -> ( [.B / y ].ph <-> [.[_z / x]_B / y ].ph))
13		nfnf1 1790	. . . . 5 |- F/x F/xph
14	13	nfal 1842	. . . 4 |- F/xA.y F/xph
15		nfa1 1788	. . . . 5 |- F/yA.y F/xph
16		nfcsb1v 3169	. . . . . 6 |- F/_x[_z / x]_B
17	16	a1i 10	. . . . 5 |- (A.y F/xph -> F/_x[_z / x]_B)
18		sp 1747	. . . . 5 |- (A.y F/xph -> F/xph)
19	15, 17, 18	nfsbcd 3067	. . . 4 |- (A.y F/xph -> F/x [.[_z / x]_B / y ].ph)
20	8, 12, 14, 19	sbciedf 3082	. . 3 |- (A.y F/xph -> ( [.z / x ]. [.B / y ].ph <-> [.[_z / x]_B / y ].ph))
21	6, 20	vtoclg 2915	. 2 |- (A e. V -> (A.y F/xph -> ( [.A / x ]. [.B / y ].ph <-> [.[_A / x]_B / y ].ph)))
22	21	imp 418	1 |- ((A e. V /\ A.y F/xph) -> ( [.A / x ]. [.B / y ].ph <-> [.[_A / x]_B / y ].ph))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540   F/wnf 1544   = wceq 1642   e. wcel 1710   F/_wnfc 2477  _Vcvv 2860   [.wsbc 3047  [_csb 3137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-sbc 3048  df-csb 3138

This theorem is referenced by:  csbnestgf  3185  sbcnestg  3186