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

Theorem nfab1 2951
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 2784 . 2 𝑥 𝑦 ∈ {𝑥𝜑}
21nfci 2936 1 𝑥{𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  {cab 2775  wnfc 2933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-10 2112
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-nfc 2935
This theorem is referenced by:  nfabd2  2970  nfabd2OLD  2971  abid2f  2980  abeq2f  2981  nfrab1  3344  elabgt  3601  elabgf  3602  elabg  3604  nfsbc1d  3724  ss2ab  3960  ab0  4253  abn0  4256  euabsn  4569  iunab  4874  iinab  4889  zfrep4  5091  sniota  6216  opabiotafun  6611  nfixp1  8330  scottexs  9162  scott0s  9163  cp  9166  ofpreima  30100  qqhval2  30840  esum2dlem  30968  sigaclcu2  30996  bnj1366  31718  bnj1321  31913  bnj1384  31918  currysetlem  33827  currysetlem1  33829  mptsnunlem  34150  topdifinffinlem  34159  scottabf  40073  compab  40313  ssfiunibd  41117  absnsb  42778  setrec2lem2  44277
  Copyright terms: Public domain W3C validator