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

Theorem nfab 2317
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 2162 . 2  |-  F/ x  z  e.  { y  |  ph }
32nfci 2302 1  |-  F/_ x { y  |  ph }
Colors of variables: wff set class
Syntax hints:   F/wnf 1453   {cab 2156   F/_wnfc 2299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-nfc 2301
This theorem is referenced by:  nfaba1  2318  nfrabxy  2650  sbcel12g  3064  sbceqg  3065  nfun  3283  nfpw  3579  nfpr  3633  nfop  3781  nfuni  3802  nfint  3841  intab  3860  nfiunxy  3899  nfiinxy  3900  nfiunya  3901  nfiinya  3902  nfiu1  3903  nfii1  3904  nfopab  4057  nfopab1  4058  nfopab2  4059  repizf2  4148  nfdm  4855  fun11iun  5463  eusvobj2  5839  nfoprab1  5902  nfoprab2  5903  nfoprab3  5904  nfoprab  5905  nfrecs  6286  nffrec  6375  nfixpxy  6695  nfixp1  6696
  Copyright terms: Public domain W3C validator