![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfab | GIF version |
Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfab.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfab | ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfab.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | nfsab 2081 | . 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑} |
3 | 2 | nfci 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 |