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

Theorem nfab1 2618
Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfab1  |-  F/_ x { x  |  ph }

Proof of Theorem nfab1
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 nfsab1 2443 . 2  |-  F/ x  y  e.  { x  |  ph }
21nfci 2605 1  |-  F/_ x { x  |  ph }
Colors of variables: wff setvar class
Syntax hints:   {cab 2439   F/_wnfc 2602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859  ax-13 2004
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-nfc 2604
This theorem is referenced by:  nfabd2  2637  abid2f  2645  abid2fOLD  2646  nfrab1  3035  elabgt  3240  elabgf  3241  nfsbc1d  3342  ss2ab  3554  abn0  3803  euabsn  4088  iunab  4361  iinab  4376  zfrep4  4558  sniota  5561  opabiotafun  5909  nfixp1  7482  scottexs  8296  scott0s  8297  cp  8300  ofpreima  27734  qqhval2  28197  esum2dlem  28321  sigaclcu2  28350  compab  31591  ssfiunibd  31748  bnj1366  34289  bnj1321  34484  bnj1384  34489
  Copyright terms: Public domain W3C validator