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

Theorem nfab1 2421
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 2273 . 2  |-  F/ x  y  e.  { x  |  ph }
21nfci 2409 1  |-  F/_ x { x  |  ph }
Colors of variables: wff set class
Syntax hints:   {cab 2269   F/_wnfc 2406
This theorem is referenced by:  nfabd2  2437  abid2f  2444  nfrab1  2720  elabgt  2911  elabgf  2912  nfsbc1d  3008  ss2ab  3241  abn0  3473  euabsn  3699  iunab  3948  iinab  3963  zfrep4  4139  sniota  5246  opabiotafun  6291  nfriota1  6312  nfixp1  6836  scottexs  7557  scott0s  7558  cp  7561  ofrn2  23207  sigaclcuni  23479  sigaclcu2  23481  compab  27644  bnj1366  28862  bnj1321  29057  bnj1384  29062
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-nfc 2408
  Copyright terms: Public domain W3C validator