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

Theorem nfab1 2907
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 2722 . 2 𝑥 𝑦 ∈ {𝑥𝜑}
21nfci 2893 1 𝑥{𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  {cab 2714  wnfc 2890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-nfc 2892
This theorem is referenced by:  nfabd2  2929  eqabf  2935  abid2fOLD  2937  nfrab1  3457  elabgf  3674  nfsbc1d  3806  ss2ab  4062  ab0ALT  4381  euabsn  4726  iunab  5051  iinab  5068  zfrep4  5293  rnep  5937  sniota  6552  opabiotafun  6989  nfixp1  8958  scottexs  9927  scott0s  9928  cp  9931  symgval  19388  ofpreima  32675  algextdeglem6  33763  qqhval2  33983  esum2dlem  34093  sigaclcu2  34121  bnj1366  34843  bnj1321  35041  bnj1384  35046  currysetlem  36946  currysetlem1  36948  bj-reabeq  37028  mptsnunlem  37339  topdifinffinlem  37348  scottabf  44259  compab  44461  ssfiunibd  45321  absnsb  47039  setrec2lem2  49213
  Copyright terms: Public domain W3C validator