![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfe1 | Structured version Visualization version Unicode version |
Description: ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfe1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbe1 1919 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nfi 1676 |
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 1671 ax-4 1684 ax-10 1917 |
This theorem depends on definitions: df-bi 189 df-ex 1666 df-nf 1670 |
This theorem is referenced by: nf3 2044 exdistrf 2169 nfmo1 2312 euor2 2345 eupicka 2368 mopick2 2371 moexex 2372 2moex 2374 2euex 2375 2moswap 2378 2mo 2382 2eu7 2390 2eu8 2391 nfre1 2850 ceqsexg 3172 morex 3224 intab 4268 nfopab1 4472 nfopab2 4473 axrep1 4519 axrep2 4520 axrep3 4521 axrep4 4522 eusv2nf 4604 copsexg 4690 copsex2t 4691 copsex2g 4692 mosubopt 4702 dfid3 4753 dmcoss 5097 imadif 5663 nfoprab1 6345 nfoprab2 6346 nfoprab3 6347 fsplit 6906 zfcndrep 9044 zfcndpow 9046 zfcndreg 9047 zfcndinf 9048 reclem2pr 9478 ex-natded9.26 25881 brabgaf 28228 bnj607 29739 bnj849 29748 bnj1398 29855 bnj1449 29869 finminlem 30986 exisym1 31096 bj-alexbiex 31305 bj-exexbiex 31306 bj-biexal2 31312 bj-biexex 31315 bj-axrep1 31415 bj-axrep2 31416 bj-axrep3 31417 bj-axrep4 31418 bj-sbf3 31451 sbexi 32363 ac6s6 32427 e2ebind 36941 e2ebindVD 37319 e2ebindALT 37336 stoweidlem57 37928 ovncvrrp 38396 |
Copyright terms: Public domain | W3C validator |