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

Theorem csbab 4395
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 2714 . . . 4 (𝑧 ∈ {𝑦[𝐴 / 𝑥]𝜑} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
2 sbsbc 3741 . . . 4 ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑[𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
31, 2bitri 274 . . 3 (𝑧 ∈ {𝑦[𝐴 / 𝑥]𝜑} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑)
4 sbccom 3825 . . . 4 ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑[𝐴 / 𝑥][𝑧 / 𝑦]𝜑)
5 df-clab 2714 . . . . . 6 (𝑧 ∈ {𝑦𝜑} ↔ [𝑧 / 𝑦]𝜑)
6 sbsbc 3741 . . . . . 6 ([𝑧 / 𝑦]𝜑[𝑧 / 𝑦]𝜑)
75, 6bitri 274 . . . . 5 (𝑧 ∈ {𝑦𝜑} ↔ [𝑧 / 𝑦]𝜑)
87sbcbii 3797 . . . 4 ([𝐴 / 𝑥]𝑧 ∈ {𝑦𝜑} ↔ [𝐴 / 𝑥][𝑧 / 𝑦]𝜑)
94, 8bitr4i 277 . . 3 ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝑧 ∈ {𝑦𝜑})
10 sbcel2 4373 . . 3 ([𝐴 / 𝑥]𝑧 ∈ {𝑦𝜑} ↔ 𝑧𝐴 / 𝑥{𝑦𝜑})
113, 9, 103bitrri 297 . 2 (𝑧𝐴 / 𝑥{𝑦𝜑} ↔ 𝑧 ∈ {𝑦[𝐴 / 𝑥]𝜑})
1211eqriv 2733 1 𝐴 / 𝑥{𝑦𝜑} = {𝑦[𝐴 / 𝑥]𝜑}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  [wsb 2067  wcel 2106  {cab 2713  [wsbc 3737  csb 3853
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 2707
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 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-nul 4281
This theorem is referenced by:  csbsng  4667  csbuni  4895  csbxp  5729  csbdm  5851  csbfrecsg  8211  csbwrdg  14424  abfmpeld  31456  abfmpel  31457  csboprabg  35768  csbfinxpg  35826  csbingVD  43108  csbsngVD  43117  csbxpgVD  43118  csbrngVD  43120  csbunigVD  43122  csbfv12gALTVD  43123
  Copyright terms: Public domain W3C validator