![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfre1 | Structured version Visualization version Unicode version |
Description: ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfre1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rex 2743 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nfe1 1918 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | nfxfr 1696 |
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-10 1915 |
This theorem depends on definitions: df-bi 189 df-ex 1664 df-nf 1668 df-rex 2743 |
This theorem is referenced by: r19.29an 2931 2rmorex 3244 nfiu1 4308 reusv2lem3 4606 elsnxp 5378 fsnex 6181 eusvobj2 6283 fun11iun 6753 zfregcl 8109 scott0 8357 ac6c4 8911 lbzbi 11252 mreiincl 15502 lss1d 18186 neiptopnei 20148 neitr 20196 utopsnneiplem 21262 cfilucfil 21574 mptelee 24925 isch3 26894 atom1d 28006 xrofsup 28353 2sqmo 28410 locfinreflem 28667 esumc 28872 esumrnmpt2 28889 hasheuni 28906 esumcvg 28907 esumcvgre 28912 voliune 29052 volfiniune 29053 ddemeas 29059 eulerpartlemgvv 29209 bnj900 29740 bnj1189 29818 bnj1204 29821 bnj1398 29843 bnj1444 29852 bnj1445 29853 bnj1446 29854 bnj1447 29855 bnj1467 29863 bnj1518 29873 bnj1519 29874 iooelexlt 31765 ptrest 31939 poimirlem26 31966 indexa 32060 filbcmb 32067 sdclem1 32072 heibor1 32142 dihglblem5 34866 suprnmpt 37439 disjinfi 37468 upbdrech 37523 ssfiunibd 37527 iccshift 37619 iooshift 37623 infrglbOLD 37669 islpcn 37719 limsupre 37721 limsupreOLD 37722 limclner 37732 itgperiod 37858 stoweidlem53 37914 stoweidlem57 37918 fourierdlem48 38018 fourierdlem51 38021 fourierdlem73 38043 fourierdlem81 38051 elaa2 38099 etransclem32 38131 sge0iunmptlemre 38257 isomenndlem 38351 ovnsubaddlem1 38392 hoidmvlelem1 38417 hoidmvlelem5 38421 reuan 38601 2reurex 38602 2reu4a 38610 2reu7 38612 2reu8 38613 2zrngagrp 39996 2zrngmmgm 39999 |
Copyright terms: Public domain | W3C validator |