Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfab | Structured version Visualization version 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 2614 | . 2 |
3 | 2 | nfci 2754 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wnf 1708 cab 2608 wnfc 2751 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-nfc 2753 |
This theorem is referenced by: nfaba1 2770 nfun 3769 sbcel12 3983 sbceqg 3984 nfpw 4172 nfpr 4232 nfuni 4442 nfint 4486 intab 4507 nfiun 4548 nfiin 4549 nfiu1 4550 nfii1 4551 nfopab 4718 nfopab1 4719 nfopab2 4720 nfdm 5367 eusvobj2 6643 nfoprab1 6704 nfoprab2 6705 nfoprab3 6706 nfoprab 6707 fun11iun 7126 nfwrecs 7409 nfixp 7927 nfixp1 7928 reclem2pr 9870 nfwrd 13333 mreiincl 16256 lss1d 18963 disjabrex 29395 disjabrexf 29396 esumc 30113 bnj900 30999 bnj1014 31030 bnj1123 31054 bnj1307 31091 bnj1398 31102 bnj1444 31111 bnj1445 31112 bnj1446 31113 bnj1447 31114 bnj1467 31122 bnj1518 31132 bnj1519 31133 dfon2lem3 31690 sdclem1 33539 heibor1 33609 dihglblem5 36587 sbcel12gOLD 38754 ssfiunibd 39523 hoidmvlelem1 40809 nfsetrecs 42433 setrec2lem2 42441 setrec2 42442 |
Copyright terms: Public domain | W3C validator |