| 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 5676 | . 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧} | |
| 2 | nfcv 2928 | . . . . 5 ⊢ Ⅎ𝑥𝑦 | |
| 3 | nfrn.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
| 4 | nfcv 2928 | . . . . 5 ⊢ Ⅎ𝑥𝑧 | |
| 5 | 2, 3, 4 | nfbr 5163 | . . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧 |
| 6 | 5 | nfex 2360 | . . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧 |
| 7 | 6 | nfab 2934 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧} |
| 8 | 1, 7 | nfcxfr 2926 | 1 ⊢ Ⅎ𝑥dom 𝐴 |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ∃wex 1812 {cab 2744 Ⅎwnfc 2913 class class class wbr 5114 dom cdm 5666 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-rab 3420 df-v 3460 df-dif 3911 df-un 3913 df-ss 3925 df-nul 4290 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-br 5115 df-dm 5676 |
| This theorem is used by: nfrn 5947 dmiin 5948 nffn 6641 nosupbnd2 27917 noinfbnd2 27932 funimass4f 33019 bnj1398 35453 bnj1491 35476 fnlimcnv 46421 fnlimfvre 46428 fnlimabslt 46433 lmbr3 46501 itgsinexplem1 46708 fourierdlem16 46877 fourierdlem21 46882 fourierdlem22 46883 fourierdlem68 46928 fourierdlem80 46940 fourierdlem103 46963 fourierdlem104 46964 issmff 47488 issmfdf 47491 smfpimltmpt 47500 smfpimltxr 47501 smfpimltxrmptf 47512 smfpreimagtf 47522 smflim 47531 smfpimgtxr 47534 smfpimgtmpt 47535 smfpimgtxrmptf 47538 smflim2 47560 smfpimcc 47562 smfsup 47568 smfsupmpt 47569 smfsupxr 47570 smfinflem 47571 smfinf 47572 smflimsup 47582 smfliminf 47585 adddmmbl2 47588 muldmmbl2 47590 smfpimne2 47594 smfdivdmmbl2 47595 fsupdm 47596 finfdm 47600 nfdfat 47904 |
| Copyright terms: Public domain | W3C validator |