MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbab Structured version   Visualization version   GIF version

Theorem csbab 4436
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.
StepHypRef Expression
1 df-clab 2710 . . . 4 (𝑧 ∈ {𝑦[𝐴 / 𝑥]𝜑} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
2 sbsbc 3780 . . . 4 ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑[𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
31, 2bitri 274 . . 3 (𝑧 ∈ {𝑦[𝐴 / 𝑥]𝜑} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
4 sbccom 3864 . . . 4 ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑[𝐴 / 𝑥][𝑧 / 𝑦]𝜑)
5 df-clab 2710 . . . . . 6 (𝑧 ∈ {𝑦𝜑} ↔ [𝑧 / 𝑦]𝜑)
6 sbsbc 3780 . . . . . 6 ([𝑧 / 𝑦]𝜑[𝑧 / 𝑦]𝜑)
75, 6bitri 274 . . . . 5 (𝑧 ∈ {𝑦𝜑} ↔ [𝑧 / 𝑦]𝜑)
87sbcbii 3836 . . . 4 ([𝐴 / 𝑥]𝑧 ∈ {𝑦𝜑} ↔ [𝐴 / 𝑥][𝑧 / 𝑦]𝜑)
94, 8bitr4i 277 . . 3 ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝑧 ∈ {𝑦𝜑})
10 sbcel2 4414 . . 3 ([𝐴 / 𝑥]𝑧 ∈ {𝑦𝜑} ↔ 𝑧𝐴 / 𝑥{𝑦𝜑})
113, 9, 103bitrri 297 . 2 (𝑧𝐴 / 𝑥{𝑦𝜑} ↔ 𝑧 ∈ {𝑦[𝐴 / 𝑥]𝜑})
1211eqriv 2729 1 𝐴 / 𝑥{𝑦𝜑} = {𝑦[𝐴 / 𝑥]𝜑}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  [wsb 2067  wcel 2106  {cab 2709  [wsbc 3776  csb 3892
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-nul 4322
This theorem is referenced by:  csbsng  4711  csbuni  4939  csbxp  5773  csbdm  5895  csbfrecsg  8265  csbwrdg  14490  abfmpeld  31866  abfmpel  31867  csboprabg  36199  csbfinxpg  36257  csbingVD  43630  csbsngVD  43639  csbxpgVD  43640  csbrngVD  43642  csbunigVD  43644  csbfv12gALTVD  43645
  Copyright terms: Public domain W3C validator