Theorem sbceqg 4353

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 3732	. . 3 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝐵 = 𝐶 ↔ [𝐴 / 𝑥]𝐵 = 𝐶))
2		dfsbcq2 3732	. . . . 5 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑦 ∈ 𝐵))
3	2	abbidv 2803	. . . 4 ⊢ (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵})
4		dfsbcq2 3732	. . . . 5 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦 ∈ 𝐶 ↔ [𝐴 / 𝑥]𝑦 ∈ 𝐶))
5	4	abbidv 2803	. . . 4 ⊢ (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶})
6	3, 5	eqeq12d 2753	. . 3 ⊢ (𝑧 = 𝐴 → ({𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}))
7		nfs1v 2162	. . . . . 6 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝑦 ∈ 𝐵
8	7	nfab 2905	. . . . 5 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵}
9		nfs1v 2162	. . . . . 6 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝑦 ∈ 𝐶
10	9	nfab 2905	. . . . 5 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶}
11	8, 10	nfeq 2913	. . . 4 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶}
12		sbab 2883	. . . . 5 ⊢ (𝑥 = 𝑧 → 𝐵 = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵})
13		sbab 2883	. . . . 5 ⊢ (𝑥 = 𝑧 → 𝐶 = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶})
14	12, 13	eqeq12d 2753	. . . 4 ⊢ (𝑥 = 𝑧 → (𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶}))
15	11, 14	sbiev 2320	. . 3 ⊢ ([𝑧 / 𝑥]𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶})
16	1, 6, 15	vtoclbg 3503	. 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}))
17		df-csb 3839	. . 3 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
18		df-csb 3839	. . 3 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}
19	17, 18	eqeq12i 2755	. 2 ⊢ (⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶})
20	16, 19	bitr4di 289	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  [wsb 2068   ∈ wcel 2114  {cab 2715  [wsbc 3729  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-sbc 3730  df-csb 3839

This theorem is referenced by:  sbceqi  4354  sbcne12  4356  sbceq1g  4358  sbceq2g  4360  csbie2df  4384  sbcfng  6661  csbfrecsg  8229  swrdspsleq  14623  fprodmodd  15957  relowlpssretop  37700  rdgeqoa  37706  poimirlem25  37986  cdlemk42  41407  minregex  43985  onfrALTlem5  44993  onfrALTlem4  44994  csbingVD  45334  onfrALTlem5VD  45335  onfrALTlem4VD  45336  csbeq2gVD  45342  csbsngVD  45343  csbunigVD  45348  csbfv12gALTVD  45349