Theorem csbnestglem 2031

Description: Lemma for csbnestg 2032.

Assertion

Ref	Expression
csbnestglem	⊢ ((A ∈ R ⋀ ∀x B ∈ S) → [A / x][B / y]C = [[A / x]B / y]C)

Distinct variable groups:   x,y,A   y,B   x,C   x,R,y   y,S

Proof of Theorem csbnestglem

Step	Hyp	Ref	Expression
1		csbiegft 2025	. 2 ⊢ ((A ∈ R ⋀ ∀x∀z(z ∈ [[A / x]B / y]C → ∀x z ∈ [[A / x]B / y]C) ⋀ ∀x(x = A → [B / y]C = [[A / x]B / y]C)) → [A / x][B / y]C = [[A / x]B / y]C)
2		pm3.26 319	. 2 ⊢ ((A ∈ R ⋀ ∀x B ∈ S) → A ∈ R)
3		ax-17 969	. . . 4 ⊢ (A ∈ R → ∀x A ∈ R)
4		hba1 1001	. . . 4 ⊢ (∀x B ∈ S → ∀x∀x B ∈ S)
5	3, 4	hban 1007	. . 3 ⊢ ((A ∈ R ⋀ ∀x B ∈ S) → ∀x(A ∈ R ⋀ ∀x B ∈ S))
6		csbexg 2004	. . . . 5 ⊢ ((A ∈ R ⋀ ∀x B ∈ S) → [A / x]B ∈ V)
7		ax-17 969	. . . . . . 7 ⊢ (A ∈ R → ∀y A ∈ R)
8		ax-17 969	. . . . . . 7 ⊢ (∀x B ∈ S → ∀y∀x B ∈ S)
9	7, 8	hban 1007	. . . . . 6 ⊢ ((A ∈ R ⋀ ∀x B ∈ S) → ∀y(A ∈ R ⋀ ∀x B ∈ S))
10		ax-17 969	. . . . . . . 8 ⊢ (z ∈ A → ∀x z ∈ A)
11	10	hbcsb1g 2020	. . . . . . 7 ⊢ (A ∈ R → (z ∈ [A / x]B → ∀x z ∈ [A / x]B))
12	11	adantr 389	. . . . . 6 ⊢ ((A ∈ R ⋀ ∀x B ∈ S) → (z ∈ [A / x]B → ∀x z ∈ [A / x]B))
13		ax-17 969	. . . . . . 7 ⊢ (z ∈ C → ∀x z ∈ C)
14	13	a1i 8	. . . . . 6 ⊢ ((A ∈ R ⋀ ∀x B ∈ S) → (z ∈ C → ∀x z ∈ C))
15	5, 9, 12, 14	hbcsbgd 2024	. . . . 5 ⊢ (((A ∈ R ⋀ ∀x B ∈ S) ⋀ [A / x]B ∈ V) → (z ∈ [[A / x]B / y]C → ∀x z ∈ [[A / x]B / y]C))
16	6, 15	mpdan 703	. . . 4 ⊢ ((A ∈ R ⋀ ∀x B ∈ S) → (z ∈ [[A / x]B / y]C → ∀x z ∈ [[A / x]B / y]C))
17	16	19.21aiv 1284	. . 3 ⊢ ((A ∈ R ⋀ ∀x B ∈ S) → ∀z(z ∈ [[A / x]B / y]C → ∀x z ∈ [[A / x]B / y]C))
18	5, 17	19.21ai 996	. 2 ⊢ ((A ∈ R ⋀ ∀x B ∈ S) → ∀x∀z(z ∈ [[A / x]B / y]C → ∀x z ∈ [[A / x]B / y]C))
19		csbeq1a 2002	. . . . 5 ⊢ (x = A → B = [A / x]B)
20	19	csbeq1d 2000	. . . 4 ⊢ (x = A → [B / y]C = [[A / x]B / y]C)
21	20	ax-gen 961	. . 3 ⊢ ∀x(x = A → [B / y]C = [[A / x]B / y]C)
22	21	a1i 8	. 2 ⊢ ((A ∈ R ⋀ ∀x B ∈ S) → ∀x(x = A → [B / y]C = [[A / x]B / y]C))
23	1, 2, 18, 22	syl3anc 857	1 ⊢ ((A ∈ R ⋀ ∀x B ∈ S) → [A / x][B / y]C = [[A / x]B / y]C)

Syntax hints:   → wi 3   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  Vcvv 1807  [csb 1997

This theorem is referenced by:  csbnestg 2032

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 776  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-sbc 1938  df-csb 1998

Copyright terms: Public domain