Theorem csbab 4388

Description: Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 19-Aug-2018.)

Assertion

Ref	Expression
csbab	⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑}

Distinct variable groups:   𝑦,𝐴   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem csbab

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-clab 2735	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝜑} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
2		sbsbc 3743	. . . 4 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
3	1, 2	bitri 277	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝜑} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
4		sbccom 3819	. . . 4 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥][𝑧 / 𝑦]𝜑)
5		df-clab 2735	. . . . . 6 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} ↔ [𝑧 / 𝑦]𝜑)
6		sbsbc 3743	. . . . . 6 ⊢ ([𝑧 / 𝑦]𝜑 ↔ [𝑧 / 𝑦]𝜑)
7	5, 6	bitri 277	. . . . 5 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} ↔ [𝑧 / 𝑦]𝜑)
8	7	sbcbii 3795	. . . 4 ⊢ ([𝐴 / 𝑥]𝑧 ∈ {𝑦 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑧 / 𝑦]𝜑)
9	4, 8	bitr4i 280	. . 3 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝑧 ∈ {𝑦 ∣ 𝜑})
10		sbcel2 4366	. . 3 ⊢ ([𝐴 / 𝑥]𝑧 ∈ {𝑦 ∣ 𝜑} ↔ 𝑧 ∈ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑})
11	3, 9, 10	3bitrri 300	. 2 ⊢ (𝑧 ∈ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝜑})
12	11	eqriv 2753	1 ⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑}

Syntax hints:   = wceq 1554  [wsb 2084   ∈ wcel 2136  {cab 2734  [wsbc 3739  ⦋csb 3847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-v 3450  df-sbc 3740  df-csb 3848  df-dif 3902  df-nul 4281

This theorem is referenced by:  csbsng  4661  csbuni  4890  csbxp  5741  csbdm  5866  csbfrecsg  8253  csbwrdg  14547  abfmpeld  32799  abfmpel  32800  csboprabg  37772  csbfinxpg  37830  csbingVD  45407  csbsngVD  45416  csbxpgVD  45417  csbrngVD  45419  csbunigVD  45421  csbfv12gALTVD  45422