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

Theorem nfab 2324
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 2169 . 2 𝑥 𝑧 ∈ {𝑦𝜑}
32nfci 2309 1 𝑥{𝑦𝜑}
Colors of variables: wff set class
Syntax hints:  wnf 1460  {cab 2163  wnfc 2306
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-nfc 2308
This theorem is referenced by:  nfaba1  2325  nfrabxy  2658  sbcel12g  3074  sbceqg  3075  nfun  3293  nfpw  3590  nfpr  3644  nfop  3796  nfuni  3817  nfint  3856  intab  3875  nfiunxy  3914  nfiinxy  3915  nfiunya  3916  nfiinya  3917  nfiu1  3918  nfii1  3919  nfopab  4073  nfopab1  4074  nfopab2  4075  repizf2  4164  nfdm  4873  fun11iun  5484  eusvobj2  5864  nfoprab1  5927  nfoprab2  5928  nfoprab3  5929  nfoprab  5930  nfrecs  6311  nffrec  6400  nfixpxy  6720  nfixp1  6721
  Copyright terms: Public domain W3C validator