| 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 5673 | . 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧} | |
| 2 | nfcv 2927 | . . . . 5 ⊢ Ⅎ𝑥𝑦 | |
| 3 | nfrn.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
| 4 | nfcv 2927 | . . . . 5 ⊢ Ⅎ𝑥𝑧 | |
| 5 | 2, 3, 4 | nfbr 5160 | . . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧 |
| 6 | 5 | nfex 2359 | . . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧 |
| 7 | 6 | nfab 2933 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧} |
| 8 | 1, 7 | nfcxfr 2925 | 1 ⊢ Ⅎ𝑥dom 𝐴 |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ∃wex 1812 {cab 2743 Ⅎwnfc 2912 class class class wbr 5111 dom cdm 5663 |
| 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 2737 |
| 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 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-rab 3419 df-v 3459 df-dif 3909 df-un 3911 df-ss 3923 df-nul 4287 df-if 4490 df-sn 4592 df-pr 4594 df-op 4598 df-br 5112 df-dm 5673 |
| This theorem is used by: nfrn 5944 dmiin 5945 nffn 6638 nosupbnd2 27933 noinfbnd2 27948 funimass4f 33055 bnj1398 35489 bnj1491 35512 fnlimcnv 46441 fnlimfvre 46448 fnlimabslt 46453 lmbr3 46521 itgsinexplem1 46728 fourierdlem16 46897 fourierdlem21 46902 fourierdlem22 46903 fourierdlem68 46948 fourierdlem80 46960 fourierdlem103 46983 fourierdlem104 46984 issmff 47508 issmfdf 47511 smfpimltmpt 47520 smfpimltxr 47521 smfpimltxrmptf 47532 smfpreimagtf 47542 smflim 47551 smfpimgtxr 47554 smfpimgtmpt 47555 smfpimgtxrmptf 47558 smflim2 47580 smfpimcc 47582 smfsup 47588 smfsupmpt 47589 smfsupxr 47590 smfinflem 47591 smfinf 47592 smflimsup 47602 smfliminf 47605 adddmmbl2 47608 muldmmbl2 47610 smfpimne2 47614 smfdivdmmbl2 47615 fsupdm 47616 finfdm 47620 nfdfat 47924 |
| Copyright terms: Public domain | W3C validator |