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

Theorem nfab 2234
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 2081 . 2 𝑥 𝑧 ∈ {𝑦𝜑}
32nfci 2219 1 𝑥{𝑦𝜑}
Colors of variables: wff set class
Syntax hints:  wnf 1395  {cab 2075  wnfc 2216
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474
This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-nfc 2218
This theorem is referenced by:  nfaba1  2235  nfrabxy  2548  sbcel12g  2947  sbceqg  2948  nfun  3157  nfpw  3446  nfpr  3496  nfop  3644  nfuni  3665  nfint  3704  intab  3723  nfiunxy  3762  nfiinxy  3763  nfiunya  3764  nfiinya  3765  nfiu1  3766  nfii1  3767  nfopab  3912  nfopab1  3913  nfopab2  3914  repizf2  4003  nfdm  4692  fun11iun  5287  eusvobj2  5652  nfoprab1  5712  nfoprab2  5713  nfoprab3  5714  nfoprab  5715  nfrecs  6086  nffrec  6175  nfixpxy  6488  nfixp1  6489
  Copyright terms: Public domain W3C validator