This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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]˙ φ