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 A V y x φ [˙A / x]˙ [˙B / y]˙ φ [˙ A / x B / y]˙ φ

Proof

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