Theorem sbceqg 4209

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 3655	. . 3 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝐵 = 𝐶 ↔ [𝐴 / 𝑥]𝐵 = 𝐶))
2		dfsbcq2 3655	. . . . 5 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑦 ∈ 𝐵))
3	2	abbidv 2906	. . . 4 ⊢ (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵})
4		dfsbcq2 3655	. . . . 5 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦 ∈ 𝐶 ↔ [𝐴 / 𝑥]𝑦 ∈ 𝐶))
5	4	abbidv 2906	. . . 4 ⊢ (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶})
6	3, 5	eqeq12d 2793	. . 3 ⊢ (𝑧 = 𝐴 → ({𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}))
7		nfs1v 2254	. . . . . 6 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝑦 ∈ 𝐵
8	7	nfab 2940	. . . . 5 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵}
9		nfs1v 2254	. . . . . 6 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝑦 ∈ 𝐶
10	9	nfab 2940	. . . . 5 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶}
11	8, 10	nfeq 2945	. . . 4 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶}
12		sbab 2918	. . . . 5 ⊢ (𝑥 = 𝑧 → 𝐵 = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵})
13		sbab 2918	. . . . 5 ⊢ (𝑥 = 𝑧 → 𝐶 = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶})
14	12, 13	eqeq12d 2793	. . . 4 ⊢ (𝑥 = 𝑧 → (𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶}))
15	11, 14	sbie 2484	. . 3 ⊢ ([𝑧 / 𝑥]𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶})
16	1, 6, 15	vtoclbg 3468	. 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}))
17		df-csb 3752	. . 3 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
18		df-csb 3752	. . 3 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}
19	17, 18	eqeq12i 2792	. 2 ⊢ (⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶})
20	16, 19	syl6bbr 281	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601  [wsb 2011   ∈ wcel 2107  {cab 2763  [wsbc 3652  ⦋csb 3751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-sbc 3653  df-csb 3752

This theorem is referenced by:  sbcne12  4211  sbceq1g  4213  sbceq2g  4215  sbcfng  6288  swrdspsleq  13769  fprodmodd  15130  csbwrecsg  33769  relowlpssretop  33807  rdgeqoa  33813  poimirlem25  34060  sbceqi  34536  cdlemk42  37095  onfrALTlem5  39702  onfrALTlem4  39703  csbingVD  40053  onfrALTlem5VD  40054  onfrALTlem4VD  40055  csbeq2gVD  40061  csbsngVD  40062  csbunigVD  40067  csbfv12gALTVD  40068