![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfdm | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Ref | Expression |
---|---|
nfrn.1 | ⊢ Ⅎ𝑥𝐴 |
Ref | Expression |
---|---|
nfdm | ⊢ Ⅎ𝑥dom 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dm 5413 | . 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧} | |
2 | nfcv 2926 | . . . . 5 ⊢ Ⅎ𝑥𝑦 | |
3 | nfrn.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
4 | nfcv 2926 | . . . . 5 ⊢ Ⅎ𝑥𝑧 | |
5 | 2, 3, 4 | nfbr 4972 | . . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧 |
6 | 5 | nfex 2264 | . . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧 |
7 | 6 | nfab 2932 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧} |
8 | 1, 7 | nfcxfr 2924 | 1 ⊢ Ⅎ𝑥dom 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∃wex 1742 {cab 2752 Ⅎwnfc 2910 class class class wbr 4925 dom cdm 5403 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-rab 3091 df-v 3411 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-br 4926 df-dm 5413 |
This theorem is referenced by: nfrn 5664 dmiin 5665 nffn 6282 funimass4f 30158 bnj1398 31980 bnj1491 32003 nosupbnd2 32766 fnlimcnv 41404 fnlimfvre 41411 fnlimabslt 41416 lmbr3 41484 itgsinexplem1 41694 fourierdlem16 41864 fourierdlem21 41869 fourierdlem22 41870 fourierdlem68 41915 fourierdlem80 41927 fourierdlem103 41950 fourierdlem104 41951 issmff 42467 issmfdf 42470 smfpimltmpt 42479 smfpimltxrmpt 42491 smfpreimagtf 42500 smflim 42509 smfpimgtxr 42512 smfpimgtmpt 42513 smfpimgtxrmpt 42516 smflim2 42536 smfpimcc 42538 smfsup 42544 smfsupmpt 42545 smfsupxr 42546 smfinflem 42547 smfinf 42548 smfinfmpt 42549 smflimsup 42558 smfliminf 42561 nfdfat 42757 |
Copyright terms: Public domain | W3C validator |