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

Metamath Proof Explorer

Theorem csbnestgf

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

Ref Expression
Assertion csbnestgf ⊢ A ∈ V ∧ ∀ y Ⅎ _ x C → ⦋ A / x⦌ ⦋ B / y⦌ C = ⦋ ⦋ A / x⦌ B / y⦌ C

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ V → A ∈ V
2 df-csb ⊢ ⦋ B / y⦌ C = z | [˙B / y]˙ z ∈ C
3 2 eqabri ⊢ z ∈ ⦋ B / y⦌ C ↔ [˙B / y]˙ z ∈ C
4 3 sbcbii ⊢ [˙A / x]˙ z ∈ ⦋ B / y⦌ C ↔ [˙A / x]˙ [˙B / y]˙ z ∈ C
5 nfcr ⊢ Ⅎ _ x C → Ⅎ x z ∈ C
6 5 alimi ⊢ ∀ y Ⅎ _ x C → ∀ y Ⅎ x z ∈ C
7 sbcnestgf ⊢ A ∈ V ∧ ∀ y Ⅎ x z ∈ C → [˙A / x]˙ [˙B / y]˙ z ∈ C ↔ [˙⦋ A / x⦌ B / y]˙ z ∈ C
8 6 7 sylan2 ⊢ A ∈ V ∧ ∀ y Ⅎ _ x C → [˙A / x]˙ [˙B / y]˙ z ∈ C ↔ [˙⦋ A / x⦌ B / y]˙ z ∈ C
9 4 8 bitrid ⊢ A ∈ V ∧ ∀ y Ⅎ _ x C → [˙A / x]˙ z ∈ ⦋ B / y⦌ C ↔ [˙⦋ A / x⦌ B / y]˙ z ∈ C
10 9 abbidv ⊢ A ∈ V ∧ ∀ y Ⅎ _ x C → z | [˙A / x]˙ z ∈ ⦋ B / y⦌ C = z | [˙⦋ A / x⦌ B / y]˙ z ∈ C
11 1 10 sylan ⊢ A ∈ V ∧ ∀ y Ⅎ _ x C → z | [˙A / x]˙ z ∈ ⦋ B / y⦌ C = z | [˙⦋ A / x⦌ B / y]˙ z ∈ C
12 df-csb ⊢ ⦋ A / x⦌ ⦋ B / y⦌ C = z | [˙A / x]˙ z ∈ ⦋ B / y⦌ C
13 df-csb ⊢ ⦋ ⦋ A / x⦌ B / y⦌ C = z | [˙⦋ A / x⦌ B / y]˙ z ∈ C
14 11 12 13 3eqtr4g ⊢ A ∈ V ∧ ∀ y Ⅎ _ x C → ⦋ A / x⦌ ⦋ B / y⦌ C = ⦋ ⦋ A / x⦌ B / y⦌ C