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

Theorem nfab1 2434
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 2286 . 2  |-  F/ x  y  e.  { x  |  ph }
21nfci 2422 1  |-  F/_ x { x  |  ph }
Colors of variables: wff set class
Syntax hints:   {cab 2282   F/_wnfc 2419
This theorem is referenced by:  nfabd2  2450  abid2f  2457  nfrab1  2733  elabgt  2924  elabgf  2925  nfsbc1d  3021  ss2ab  3254  abn0  3486  euabsn  3712  iunab  3964  iinab  3979  zfrep4  4155  sniota  5262  opabiotafun  6307  nfriota1  6328  nfixp1  6852  scottexs  7573  scott0s  7574  cp  7577  ofrn2  23222  sigaclcuni  23494  sigaclcu2  23496  compab  27747  bnj1366  29178  bnj1321  29373  bnj1384  29378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-nfc 2421
  Copyright terms: Public domain W3C validator