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

Theorem nfab 2233
Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfab.1 𝑥𝜑
Assertion
Ref Expression
nfab 𝑥{𝑦𝜑}

Proof of Theorem nfab
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 nfab.1 . . 3 𝑥𝜑
21nfsab 2080 . 2 𝑥 𝑧 ∈ {𝑦𝜑}
32nfci 2218 1 𝑥{𝑦𝜑}
Colors of variables: wff set class
Syntax hints:  wnf 1394  {cab 2074  wnfc 2215
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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-nfc 2217
This theorem is referenced by:  nfaba1  2234  nfrabxy  2547  sbcel12g  2944  sbceqg  2945  nfun  3154  nfpw  3437  nfpr  3487  nfop  3633  nfuni  3654  nfint  3693  intab  3712  nfiunxy  3751  nfiinxy  3752  nfiunya  3753  nfiinya  3754  nfiu1  3755  nfii1  3756  nfopab  3898  nfopab1  3899  nfopab2  3900  repizf2  3989  nfdm  4667  fun11iun  5258  eusvobj2  5620  nfoprab1  5680  nfoprab2  5681  nfoprab3  5682  nfoprab  5683  nfrecs  6054  nffrec  6143
  Copyright terms: Public domain W3C validator