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

Theorem nfab1 2621
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 2446 . 2
21nfci 2608 1
Colors of variables: wff setvar class
Syntax hints:  {cab 2442  F/_wnfc 2605
This theorem is referenced by:  nfabd2  2640  abid2f  2648  abid2fOLD  2649  nfrab1  3038  elabgt  3243  elabgf  3244  nfsbc1d  3345  ss2ab  3567  abn0  3804  euabsn  4102  iunab  4376  iinab  4391  zfrep4  4571  sniota  5583  opabiotafun  5934  nfixp1  7509  scottexs  8326  scott0s  8327  cp  8330  ofpreima  27507  qqhval2  27963  sigaclcu2  28120  compab  31350  ssfiunibd  31509  bnj1366  33888  bnj1321  34083  bnj1384  34088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-13 1999
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-nfc 2607
  Copyright terms: Public domain W3C validator