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 5640 | . 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧} | |
2 | nfcv 2905 | . . . . 5 ⊢ Ⅎ𝑥𝑦 | |
3 | nfrn.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
4 | nfcv 2905 | . . . . 5 ⊢ Ⅎ𝑥𝑧 | |
5 | 2, 3, 4 | nfbr 5150 | . . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧 |
6 | 5 | nfex 2318 | . . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧 |
7 | 6 | nfab 2911 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧} |
8 | 1, 7 | nfcxfr 2903 | 1 ⊢ Ⅎ𝑥dom 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∃wex 1781 {cab 2714 Ⅎwnfc 2885 class class class wbr 5103 dom cdm 5630 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-dm 5640 |
This theorem is referenced by: nfrn 5903 dmiin 5904 nffn 6596 nosupbnd2 26986 noinfbnd2 27001 funimass4f 31348 bnj1398 33419 bnj1491 33442 fnlimcnv 43661 fnlimfvre 43668 fnlimabslt 43673 lmbr3 43741 itgsinexplem1 43948 fourierdlem16 44117 fourierdlem21 44122 fourierdlem22 44123 fourierdlem68 44168 fourierdlem80 44180 fourierdlem103 44203 fourierdlem104 44204 issmff 44728 issmfdf 44731 smfpimltmpt 44740 smfpimltxr 44741 smfpimltxrmptf 44752 smfpreimagtf 44762 smflim 44771 smfpimgtxr 44774 smfpimgtmpt 44775 smfpimgtxrmptf 44778 smflim2 44800 smfpimcc 44802 smfsup 44808 smfsupmpt 44809 smfsupxr 44810 smfinflem 44811 smfinf 44812 smfinfmpt 44813 smflimsup 44822 smfliminf 44825 adddmmbl2 44828 muldmmbl2 44830 smfpimne2 44834 smfdivdmmbl2 44835 fsupdm 44836 nfdfat 45108 |
Copyright terms: Public domain | W3C validator |