Theorem csbnestgf 3184

Description: Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)

Assertion

Ref	Expression
csbnestgf	⊢ ((A ∈ V ∧ ∀yℲxC) → [A / x][B / y]C = [[A / x]B / y]C)

Proof of Theorem csbnestgf

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2867	. . 3 ⊢ (A ∈ V → A ∈ V)
2		df-csb 3137	. . . . . . 7 ⊢ [B / y]C = {z ∣ [̣B / y]̣z ∈ C}
3	2	abeq2i 2460	. . . . . 6 ⊢ (z ∈ [B / y]C ↔ [̣B / y]̣z ∈ C)
4	3	sbcbii 3101	. . . . 5 ⊢ ([̣A / x]̣z ∈ [B / y]C ↔ [̣A / x]̣[̣B / y]̣z ∈ C)
5		nfcr 2481	. . . . . . 7 ⊢ (ℲxC → Ⅎx z ∈ C)
6	5	alimi 1559	. . . . . 6 ⊢ (∀yℲxC → ∀yℲx z ∈ C)
7		sbcnestgf 3183	. . . . . 6 ⊢ ((A ∈ V ∧ ∀yℲx z ∈ C) → ([̣A / x]̣[̣B / y]̣z ∈ C ↔ [̣[A / x]B / y]̣z ∈ C))
8	6, 7	sylan2 460	. . . . 5 ⊢ ((A ∈ V ∧ ∀yℲxC) → ([̣A / x]̣[̣B / y]̣z ∈ C ↔ [̣[A / x]B / y]̣z ∈ C))
9	4, 8	syl5bb 248	. . . 4 ⊢ ((A ∈ V ∧ ∀yℲxC) → ([̣A / x]̣z ∈ [B / y]C ↔ [̣[A / x]B / y]̣z ∈ C))
10	9	abbidv 2467	. . 3 ⊢ ((A ∈ V ∧ ∀yℲxC) → {z ∣ [̣A / x]̣z ∈ [B / y]C} = {z ∣ [̣[A / x]B / y]̣z ∈ C})
11	1, 10	sylan 457	. 2 ⊢ ((A ∈ V ∧ ∀yℲxC) → {z ∣ [̣A / x]̣z ∈ [B / y]C} = {z ∣ [̣[A / x]B / y]̣z ∈ C})
12		df-csb 3137	. 2 ⊢ [A / x][B / y]C = {z ∣ [̣A / x]̣z ∈ [B / y]C}
13		df-csb 3137	. 2 ⊢ [[A / x]B / y]C = {z ∣ [̣[A / x]B / y]̣z ∈ C}
14	11, 12, 13	3eqtr4g 2410	1 ⊢ ((A ∈ V ∧ ∀yℲxC) → [A / x][B / y]C = [[A / x]B / y]C)

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  Ⅎwnf 1544   = wceq 1642   ∈ wcel 1710  {cab 2339  Ⅎwnfc 2476  Vcvv 2859  [̣wsbc 3046  [csb 3136

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 2478  df-v 2861  df-sbc 3047  df-csb 3137

This theorem is referenced by:  csbnestg  3186  csbnest1g  3188