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

Theorem nfab1 2906
Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfab1 𝑥{𝑥𝜑}

Proof of Theorem nfab1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 nfsab1 2718 . 2 𝑥 𝑦 ∈ {𝑥𝜑}
21nfci 2887 1 𝑥{𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  {cab 2710  wnfc 2884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-nfc 2886
This theorem is referenced by:  nfabd2  2930  abid2f  2936  eqabf  2937  nfrab1  3425  elabgtOLD  3629  elabgf  3630  elabgOLD  3633  nfsbc1d  3761  ss2ab  4020  ab0ALT  4340  abn0OLD  4345  euabsn  4691  iunab  5015  iinab  5032  zfrep4  5257  rnep  5886  sniota  6491  opabiotafun  6926  nfixp1  8862  scottexs  9831  scott0s  9832  cp  9835  symgval  19158  ofpreima  31634  qqhval2  32627  esum2dlem  32755  sigaclcu2  32783  bnj1366  33505  bnj1321  33703  bnj1384  33708  currysetlem  35466  currysetlem1  35468  bj-reabeq  35548  mptsnunlem  35859  topdifinffinlem  35868  scottabf  42612  compab  42814  ssfiunibd  43634  absnsb  45351  setrec2lem2  47229
  Copyright terms: Public domain W3C validator