![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfrab | Structured version Visualization version Unicode version |
Description: A variable not free in a wff remains so in a restricted class abstraction. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.) |
Ref | Expression |
---|---|
nfrab.1 |
![]() ![]() ![]() ![]() |
nfrab.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfrab |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rab 2758 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nftru 1688 |
. . . 4
![]() ![]() ![]() ![]() | |
3 | nfrab.2 |
. . . . . . . 8
![]() ![]() ![]() ![]() | |
4 | 3 | nfcri 2597 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() |
5 | eleq1 2528 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | dvelimnf 2184 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | nfrab.1 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
8 | 7 | a1i 11 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 6, 8 | nfand 2019 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | adantl 472 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 2, 10 | nfabd2 2622 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11 | trud 1464 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 1, 12 | nfcxfr 2601 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-rab 2758 |
This theorem is referenced by: nfdif 3566 nfin 3651 nfse 4831 elfvmptrab1 5998 elovmpt2rab 6547 elovmpt2rab1 6548 ovmpt3rab1 6557 elovmpt3rab1 6559 mpt2xopoveq 6997 nfoi 8060 scottex 8387 elmptrab 20897 iundisjf 28253 nnindf 28434 bnj1398 29893 bnj1445 29903 bnj1449 29907 nfwlim 30555 finminlem 31024 poimirlem26 32012 poimirlem27 32013 indexa 32106 binomcxplemdvbinom 36747 binomcxplemdvsum 36749 binomcxplemnotnn0 36750 dvnprodlem1 37907 stoweidlem16 37977 stoweidlem31 37993 stoweidlem34 37996 stoweidlem35 37997 stoweidlem48 38010 stoweidlem51 38013 stoweidlem53 38015 stoweidlem54 38016 stoweidlem57 38019 stoweidlem59 38021 fourierdlem31 38101 fourierdlem31OLD 38102 fourierdlem48 38119 fourierdlem51 38122 etransclem32 38232 ovncvrrp 38493 |
Copyright terms: Public domain | W3C validator |