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

Theorem nfsab1 2811
 Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove use of ax-12 2179. (Revised by SN, 20-Sep-2023.)
Assertion
Ref Expression
nfsab1 𝑥 𝑦 ∈ {𝑥𝜑}
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem nfsab1
StepHypRef Expression
1 df-clab 2803 . 2 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
2 nfs1v 2161 . 2 𝑥[𝑦 / 𝑥]𝜑
31, 2nfxfr 1854 1 𝑥 𝑦 ∈ {𝑥𝜑}
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnf 1785  [wsb 2070   ∈ wcel 2115  {cab 2802 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 1912  ax-6 1971  ax-7 2016  ax-10 2146 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803 This theorem is referenced by:  abbi  2891  clelab  2959  nfab1  2984  ralab2  3674  ralab2OLD  3675  rexab2  3677  rexab2OLD  3678  eluniab  4839  elintab  4873  opabex3d  7661  opabex3rd  7662  opabex3  7663  setindtrs  39882  rababg  40189  scottabf  40868
 Copyright terms: Public domain W3C validator