Metamath Proof Explorer


Theorem sbcnestgf

Description: Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sbcnestgfw when possible. (Contributed by Mario Carneiro, 11-Nov-2016) (New usage is discouraged.)

Ref Expression
Assertion sbcnestgf AVyxφ[˙A/x]˙[˙B/y]˙φ[˙A/xB/y]˙φ

Proof

Step Hyp Ref Expression
1 dfsbcq z=A[˙z/x]˙[˙B/y]˙φ[˙A/x]˙[˙B/y]˙φ
2 csbeq1 z=Az/xB=A/xB
3 2 sbceq1d z=A[˙z/xB/y]˙φ[˙A/xB/y]˙φ
4 1 3 bibi12d z=A[˙z/x]˙[˙B/y]˙φ[˙z/xB/y]˙φ[˙A/x]˙[˙B/y]˙φ[˙A/xB/y]˙φ
5 4 imbi2d z=Ayxφ[˙z/x]˙[˙B/y]˙φ[˙z/xB/y]˙φyxφ[˙A/x]˙[˙B/y]˙φ[˙A/xB/y]˙φ
6 vex zV
7 6 a1i yxφzV
8 csbeq1a x=zB=z/xB
9 8 sbceq1d x=z[˙B/y]˙φ[˙z/xB/y]˙φ
10 9 adantl yxφx=z[˙B/y]˙φ[˙z/xB/y]˙φ
11 nfnf1 xxφ
12 11 nfal xyxφ
13 nfa1 yyxφ
14 nfcsb1v _xz/xB
15 14 a1i yxφ_xz/xB
16 sp yxφxφ
17 13 15 16 nfsbcd yxφx[˙z/xB/y]˙φ
18 7 10 12 17 sbciedf yxφ[˙z/x]˙[˙B/y]˙φ[˙z/xB/y]˙φ
19 5 18 vtoclg AVyxφ[˙A/x]˙[˙B/y]˙φ[˙A/xB/y]˙φ
20 19 imp AVyxφ[˙A/x]˙[˙B/y]˙φ[˙A/xB/y]˙φ