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

Theorem nfsab1 2805
Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove use of ax-12 2167. (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 2797 . 2 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
2 nfs1v 2264 . 2 𝑥[𝑦 / 𝑥]𝜑
31, 2nfxfr 1844 1 𝑥 𝑦 ∈ {𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  wnf 1775  [wsb 2060  wcel 2105  {cab 2796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-10 2136
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797
This theorem is referenced by:  abbi  2885  clelab  2955  nfab1  2976  ralab2  3685  ralab2OLD  3686  rexab2  3688  rexab2OLD  3689  eluniab  4841  elintab  4878  opabex3d  7655  opabex3rd  7656  opabex3  7657  setindtrs  39500  rababg  39811  scottabf  40453
  Copyright terms: Public domain W3C validator