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

Theorem nfab1 2897
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 2709 . 2 𝑥 𝑦 ∈ {𝑥𝜑}
21nfci 2878 1 𝑥{𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  {cab 2701  wnfc 2875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2702  df-nfc 2877
This theorem is referenced by:  nfabd2  2921  eqabf  2927  abid2fOLD  2929  nfrab1  3443  elabgtOLD  3655  elabgf  3656  elabgOLD  3659  nfsbc1d  3787  ss2ab  4048  ab0ALT  4368  abn0OLD  4373  euabsn  4722  iunab  5044  iinab  5061  zfrep4  5286  rnep  5916  sniota  6524  opabiotafun  6962  nfixp1  8907  scottexs  9877  scott0s  9878  cp  9881  symgval  19273  ofpreima  32314  algextdeglem6  33224  qqhval2  33417  esum2dlem  33545  sigaclcu2  33573  bnj1366  34295  bnj1321  34493  bnj1384  34498  currysetlem  36282  currysetlem1  36284  bj-reabeq  36364  mptsnunlem  36675  topdifinffinlem  36684  scottabf  43454  compab  43656  ssfiunibd  44470  absnsb  46188  setrec2lem2  47893
  Copyright terms: Public domain W3C validator