Theorem csbab 4391

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

Syntax hints:   = wceq 1541  [wsb 2067   ∈ wcel 2113  {cab 2711  [wsbc 3738  ⦋csb 3847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-nul 4285

This theorem is referenced by:  csbsng  4662  csbuni  4890  csbxp  5722  csbdm  5844  csbfrecsg  8223  csbwrdg  14461  abfmpeld  32647  abfmpel  32648  csboprabg  37385  csbfinxpg  37443  csbingVD  44990  csbsngVD  44999  csbxpgVD  45000  csbrngVD  45002  csbunigVD  45004  csbfv12gALTVD  45005