Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfab | Unicode 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 2149 | . 2 |
3 | 2 | nfci 2289 | 1 |
Colors of variables: wff set class |
Syntax hints: wnf 1440 cab 2143 wnfc 2286 |
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 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 |
This theorem depends on definitions: df-bi 116 df-nf 1441 df-sb 1743 df-clab 2144 df-nfc 2288 |
This theorem is referenced by: nfaba1 2305 nfrabxy 2637 sbcel12g 3046 sbceqg 3047 nfun 3264 nfpw 3557 nfpr 3611 nfop 3759 nfuni 3780 nfint 3819 intab 3838 nfiunxy 3877 nfiinxy 3878 nfiunya 3879 nfiinya 3880 nfiu1 3881 nfii1 3882 nfopab 4034 nfopab1 4035 nfopab2 4036 repizf2 4125 nfdm 4832 fun11iun 5437 eusvobj2 5812 nfoprab1 5872 nfoprab2 5873 nfoprab3 5874 nfoprab 5875 nfrecs 6256 nffrec 6345 nfixpxy 6664 nfixp1 6665 |
Copyright terms: Public domain | W3C validator |