![]() |
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 1952 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | hbex 2029 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | nfi 1674 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 df-nf 1668 |
This theorem is referenced by: 19.12 2033 eeor 2056 eean 2077 eeeanv 2079 nfeu1 2309 moexex 2370 ceqsex2 3086 nfopab 4468 nfopab2 4470 cbvopab1 4473 cbvopab1s 4475 axrep2 4517 axrep3 4518 axrep4 4519 copsex2t 4688 copsex2g 4689 mosubopt 4699 euotd 4702 nfco 5000 dfdmf 5028 dfrnf 5073 nfdm 5076 fv3 5878 oprabv 6339 nfoprab2 6341 nfoprab3 6342 nfoprab 6343 cbvoprab1 6363 cbvoprab2 6364 cbvoprab3 6367 nfwrecs 7030 ac6sfi 7815 aceq1 8548 zfcndrep 9039 zfcndinf 9043 nfsum1 13756 nfsum 13757 fsum2dlem 13831 nfcprod1 13964 nfcprod 13965 fprod2dlem 14034 brabgaf 28216 cnvoprab 28308 bnj981 29761 bnj1388 29842 bnj1445 29853 bnj1489 29865 bj-axrep2 31404 bj-axrep3 31405 bj-axrep4 31406 pm11.71 36747 upbdrech 37523 stoweidlem57 37918 |
Copyright terms: Public domain | W3C validator |