Theorem sbceqg 4417

Description: Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Assertion

Ref	Expression
sbceqg	⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))

Proof of Theorem sbceqg

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsbcq2 3793	. . 3 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝐵 = 𝐶 ↔ [𝐴 / 𝑥]𝐵 = 𝐶))
2		dfsbcq2 3793	. . . . 5 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑦 ∈ 𝐵))
3	2	abbidv 2805	. . . 4 ⊢ (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵})
4		dfsbcq2 3793	. . . . 5 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦 ∈ 𝐶 ↔ [𝐴 / 𝑥]𝑦 ∈ 𝐶))
5	4	abbidv 2805	. . . 4 ⊢ (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶})
6	3, 5	eqeq12d 2750	. . 3 ⊢ (𝑧 = 𝐴 → ({𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}))
7		nfs1v 2153	. . . . . 6 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝑦 ∈ 𝐵
8	7	nfab 2908	. . . . 5 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵}
9		nfs1v 2153	. . . . . 6 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝑦 ∈ 𝐶
10	9	nfab 2908	. . . . 5 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶}
11	8, 10	nfeq 2916	. . . 4 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶}
12		sbab 2886	. . . . 5 ⊢ (𝑥 = 𝑧 → 𝐵 = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵})
13		sbab 2886	. . . . 5 ⊢ (𝑥 = 𝑧 → 𝐶 = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶})
14	12, 13	eqeq12d 2750	. . . 4 ⊢ (𝑥 = 𝑧 → (𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶}))
15	11, 14	sbiev 2312	. . 3 ⊢ ([𝑧 / 𝑥]𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶})
16	1, 6, 15	vtoclbg 3556	. 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}))
17		df-csb 3908	. . 3 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
18		df-csb 3908	. . 3 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}
19	17, 18	eqeq12i 2752	. 2 ⊢ (⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶})
20	16, 19	bitr4di 289	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  [wsb 2061   ∈ wcel 2105  {cab 2711  [wsbc 3790  ⦋csb 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-sbc 3791  df-csb 3908

This theorem is referenced by:  sbceqi  4418  sbcne12  4420  sbceq1g  4422  sbceq2g  4424  csbie2df  4448  sbcfng  6733  csbfrecsg  8307  swrdspsleq  14699  fprodmodd  16029  relowlpssretop  37346  rdgeqoa  37352  poimirlem25  37631  cdlemk42  40923  minregex  43523  onfrALTlem5  44539  onfrALTlem4  44540  csbingVD  44881  onfrALTlem5VD  44882  onfrALTlem4VD  44883  csbeq2gVD  44889  csbsngVD  44890  csbunigVD  44895  csbfv12gALTVD  44896