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 5561 | . 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧} | |
2 | nfcv 2904 | . . . . 5 ⊢ Ⅎ𝑥𝑦 | |
3 | nfrn.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
4 | nfcv 2904 | . . . . 5 ⊢ Ⅎ𝑥𝑧 | |
5 | 2, 3, 4 | nfbr 5100 | . . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧 |
6 | 5 | nfex 2323 | . . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧 |
7 | 6 | nfab 2910 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧} |
8 | 1, 7 | nfcxfr 2902 | 1 ⊢ Ⅎ𝑥dom 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∃wex 1787 {cab 2714 Ⅎwnfc 2884 class class class wbr 5053 dom cdm 5551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-br 5054 df-dm 5561 |
This theorem is referenced by: nfrn 5821 dmiin 5822 nffn 6478 funimass4f 30691 bnj1398 32727 bnj1491 32750 nosupbnd2 33656 noinfbnd2 33671 fnlimcnv 42883 fnlimfvre 42890 fnlimabslt 42895 lmbr3 42963 itgsinexplem1 43170 fourierdlem16 43339 fourierdlem21 43344 fourierdlem22 43345 fourierdlem68 43390 fourierdlem80 43402 fourierdlem103 43425 fourierdlem104 43426 issmff 43942 issmfdf 43945 smfpimltmpt 43954 smfpimltxrmpt 43966 smfpreimagtf 43975 smflim 43984 smfpimgtxr 43987 smfpimgtmpt 43988 smfpimgtxrmpt 43991 smflim2 44011 smfpimcc 44013 smfsup 44019 smfsupmpt 44020 smfsupxr 44021 smfinflem 44022 smfinf 44023 smfinfmpt 44024 smflimsup 44033 smfliminf 44036 nfdfat 44291 |
Copyright terms: Public domain | W3C validator |