ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfab Unicode version

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

Proof of Theorem nfab
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 nfab.1 . . 3  |-  F/ x ph
21nfsab 2074 . 2  |-  F/ x  z  e.  { y  |  ph }
32nfci 2210 1  |-  F/_ x { y  |  ph }
Colors of variables: wff set class
Syntax hints:   F/wnf 1390   {cab 2068   F/_wnfc 2207
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-nfc 2209
This theorem is referenced by:  nfaba1  2225  nfrabxy  2535  sbcel12g  2922  sbceqg  2923  nfun  3129  nfpw  3402  nfpr  3450  nfop  3594  nfuni  3615  nfint  3654  intab  3673  nfiunxy  3712  nfiinxy  3713  nfiunya  3714  nfiinya  3715  nfiu1  3716  nfii1  3717  nfopab  3854  nfopab1  3855  nfopab2  3856  repizf2  3944  nfdm  4606  fun11iun  5178  eusvobj2  5529  nfoprab1  5585  nfoprab2  5586  nfoprab3  5587  nfoprab  5588  nfrecs  5956  nffrec  6045
  Copyright terms: Public domain W3C validator