Theorem csbab 4411

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 2709	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝜑} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
2		sbsbc 3765	. . . 4 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
3	1, 2	bitri 275	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝜑} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
4		sbccom 3842	. . . 4 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥][𝑧 / 𝑦]𝜑)
5		df-clab 2709	. . . . . 6 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} ↔ [𝑧 / 𝑦]𝜑)
6		sbsbc 3765	. . . . . 6 ⊢ ([𝑧 / 𝑦]𝜑 ↔ [𝑧 / 𝑦]𝜑)
7	5, 6	bitri 275	. . . . 5 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} ↔ [𝑧 / 𝑦]𝜑)
8	7	sbcbii 3818	. . . 4 ⊢ ([𝐴 / 𝑥]𝑧 ∈ {𝑦 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑧 / 𝑦]𝜑)
9	4, 8	bitr4i 278	. . 3 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝑧 ∈ {𝑦 ∣ 𝜑})
10		sbcel2 4389	. . 3 ⊢ ([𝐴 / 𝑥]𝑧 ∈ {𝑦 ∣ 𝜑} ↔ 𝑧 ∈ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑})
11	3, 9, 10	3bitrri 298	. 2 ⊢ (𝑧 ∈ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝜑})
12	11	eqriv 2727	1 ⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑}

Syntax hints:   = wceq 1540  [wsb 2065   ∈ wcel 2109  {cab 2708  [wsbc 3761  ⦋csb 3870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2880  df-v 3457  df-sbc 3762  df-csb 3871  df-dif 3925  df-nul 4305

This theorem is referenced by:  csbsng  4680  csbuni  4908  csbxp  5746  csbdm  5869  csbfrecsg  8272  csbwrdg  14519  abfmpeld  32586  abfmpel  32587  csboprabg  37315  csbfinxpg  37373  csbingVD  44845  csbsngVD  44854  csbxpgVD  44855  csbrngVD  44857  csbunigVD  44859  csbfv12gALTVD  44860