Theorem sbcnestg 2034

Description: Nest the composition of two substitutions.

Assertion

Ref	Expression
sbcnestg	⊢ ((A ∈ R ⋀ ∀x B ∈ S) → ([A / x][B / y]φ ↔ [[A / x]B / y]φ))

Distinct variable groups:   φ,x   x,y

Proof of Theorem sbcnestg

Step	Hyp	Ref	Expression
1		hba1 1001	. . . . 5 ⊢ (∀x B ∈ V → ∀x∀x B ∈ V)
2		sbccsb2g 2019	. . . . . 6 ⊢ (B ∈ V → ([B / y]φ ↔ B ∈ [B / y]{y∣φ}))
3	2	a4s 982	. . . . 5 ⊢ (∀x B ∈ V → ([B / y]φ ↔ B ∈ [B / y]{y∣φ}))
4	1, 3	sbcbid 1972	. . . 4 ⊢ ((∀x B ∈ V ⋀ A ∈ R) → ([A / x][B / y]φ ↔ [A / x]B ∈ [B / y]{y∣φ}))
5	4	ancoms 436	. . 3 ⊢ ((A ∈ R ⋀ ∀x B ∈ V) → ([A / x][B / y]φ ↔ [A / x]B ∈ [B / y]{y∣φ}))
6		sbcel12g 2007	. . . 4 ⊢ (A ∈ R → ([A / x]B ∈ [B / y]{y∣φ} ↔ [A / x]B ∈ [A / x][B / y]{y∣φ}))
7	6	adantr 389	. . 3 ⊢ ((A ∈ R ⋀ ∀x B ∈ V) → ([A / x]B ∈ [B / y]{y∣φ} ↔ [A / x]B ∈ [A / x][B / y]{y∣φ}))
8		csbnestg 2032	. . . . 5 ⊢ ((A ∈ R ⋀ ∀x B ∈ V) → [A / x][B / y]{y∣φ} = [[A / x]B / y]{y∣φ})
9	8	eleq2d 1538	. . . 4 ⊢ ((A ∈ R ⋀ ∀x B ∈ V) → ([A / x]B ∈ [A / x][B / y]{y∣φ} ↔ [A / x]B ∈ [[A / x]B / y]{y∣φ}))
10		csbexg 2004	. . . . 5 ⊢ ((A ∈ R ⋀ ∀x B ∈ V) → [A / x]B ∈ V)
11		sbccsb2g 2019	. . . . 5 ⊢ ([A / x]B ∈ V → ([[A / x]B / y]φ ↔ [A / x]B ∈ [[A / x]B / y]{y∣φ}))
12	10, 11	syl 10	. . . 4 ⊢ ((A ∈ R ⋀ ∀x B ∈ V) → ([[A / x]B / y]φ ↔ [A / x]B ∈ [[A / x]B / y]{y∣φ}))
13	9, 12	bitr4d 530	. . 3 ⊢ ((A ∈ R ⋀ ∀x B ∈ V) → ([A / x]B ∈ [A / x][B / y]{y∣φ} ↔ [[A / x]B / y]φ))
14	5, 7, 13	3bitrd 543	. 2 ⊢ ((A ∈ R ⋀ ∀x B ∈ V) → ([A / x][B / y]φ ↔ [[A / x]B / y]φ))
15		elisset 1813	. . 3 ⊢ (B ∈ S → B ∈ V)
16	15	19.20i 990	. 2 ⊢ (∀x B ∈ S → ∀x B ∈ V)
17	14, 16	sylan2 451	1 ⊢ ((A ∈ R ⋀ ∀x B ∈ S) → ([A / x][B / y]φ ↔ [[A / x]B / y]φ))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 952   ∈ wcel 956  [wsbc 1168  {cab 1461  Vcvv 1807  [csb 1997

This theorem is referenced by:  sbcco3g 2037

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