![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfex | Structured version Visualization version Unicode version |
Description: If ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfal.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfex |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfal.1 |
. . . 4
![]() ![]() ![]() ![]() | |
2 | 1 | nfri 1972 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | hbex 2048 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | nfi 1682 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 |
This theorem depends on definitions: df-bi 190 df-ex 1672 df-nf 1676 |
This theorem is referenced by: 19.12 2052 eeor 2075 eean 2092 eeeanv 2094 nfeu1 2329 moexex 2390 ceqsex2 3072 nfopab 4461 nfopab2 4463 cbvopab1 4466 cbvopab1s 4468 axrep2 4510 axrep3 4511 axrep4 4512 copsex2t 4688 copsex2g 4689 mosubopt 4699 euotd 4702 nfco 5005 dfdmf 5033 dfrnf 5079 nfdm 5082 fv3 5892 oprabv 6358 nfoprab2 6360 nfoprab3 6361 nfoprab 6362 cbvoprab1 6382 cbvoprab2 6383 cbvoprab3 6386 nfwrecs 7048 ac6sfi 7833 aceq1 8566 zfcndrep 9057 zfcndinf 9061 nfsum1 13833 nfsum 13834 fsum2dlem 13908 nfcprod1 14041 nfcprod 14042 fprod2dlem 14111 brabgaf 28292 cnvoprab 28383 bnj981 29833 bnj1388 29914 bnj1445 29925 bnj1489 29937 bj-axrep2 31470 bj-axrep3 31471 bj-axrep4 31472 pm11.71 36817 upbdrech 37611 stoweidlem57 38030 |
Copyright terms: Public domain | W3C validator |