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

Theorem csbab 4348
 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 2780 . . . 4 (𝑧 ∈ {𝑦[𝐴 / 𝑥]𝜑} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
2 sbsbc 3727 . . . 4 ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑[𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
31, 2bitri 278 . . 3 (𝑧 ∈ {𝑦[𝐴 / 𝑥]𝜑} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
4 sbccom 3803 . . . 4 ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑[𝐴 / 𝑥][𝑧 / 𝑦]𝜑)
5 df-clab 2780 . . . . . 6 (𝑧 ∈ {𝑦𝜑} ↔ [𝑧 / 𝑦]𝜑)
6 sbsbc 3727 . . . . . 6 ([𝑧 / 𝑦]𝜑[𝑧 / 𝑦]𝜑)
75, 6bitri 278 . . . . 5 (𝑧 ∈ {𝑦𝜑} ↔ [𝑧 / 𝑦]𝜑)
87sbcbii 3779 . . . 4 ([𝐴 / 𝑥]𝑧 ∈ {𝑦𝜑} ↔ [𝐴 / 𝑥][𝑧 / 𝑦]𝜑)
94, 8bitr4i 281 . . 3 ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝑧 ∈ {𝑦𝜑})
10 sbcel2 4326 . . 3 ([𝐴 / 𝑥]𝑧 ∈ {𝑦𝜑} ↔ 𝑧𝐴 / 𝑥{𝑦𝜑})
113, 9, 103bitrri 301 . 2 (𝑧𝐴 / 𝑥{𝑦𝜑} ↔ 𝑧 ∈ {𝑦[𝐴 / 𝑥]𝜑})
1211eqriv 2798 1 𝐴 / 𝑥{𝑦𝜑} = {𝑦[𝐴 / 𝑥]𝜑}
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538  [wsb 2069   ∈ wcel 2112  {cab 2779  [wsbc 3723  ⦋csb 3831 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-nul 4247 This theorem is referenced by:  csbsng  4607  csbuni  4832  csbxp  5618  csbdm  5734  csbwrdg  13891  abfmpeld  30420  abfmpel  30421  csbwrecsg  34739  csboprabg  34742  csbfinxpg  34800  csbingVD  41577  csbsngVD  41586  csbxpgVD  41587  csbrngVD  41589  csbunigVD  41591  csbfv12gALTVD  41592
 Copyright terms: Public domain W3C validator