![]() |
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 5686 | . 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧} | |
2 | nfcv 2902 | . . . . 5 ⊢ Ⅎ𝑥𝑦 | |
3 | nfrn.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
4 | nfcv 2902 | . . . . 5 ⊢ Ⅎ𝑥𝑧 | |
5 | 2, 3, 4 | nfbr 5195 | . . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧 |
6 | 5 | nfex 2316 | . . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧 |
7 | 6 | nfab 2908 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧} |
8 | 1, 7 | nfcxfr 2900 | 1 ⊢ Ⅎ𝑥dom 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∃wex 1780 {cab 2708 Ⅎwnfc 2882 class class class wbr 5148 dom cdm 5676 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-dm 5686 |
This theorem is referenced by: nfrn 5951 dmiin 5952 nffn 6648 nosupbnd2 27562 noinfbnd2 27577 funimass4f 32294 bnj1398 34509 bnj1491 34532 fnlimcnv 44842 fnlimfvre 44849 fnlimabslt 44854 lmbr3 44922 itgsinexplem1 45129 fourierdlem16 45298 fourierdlem21 45303 fourierdlem22 45304 fourierdlem68 45349 fourierdlem80 45361 fourierdlem103 45384 fourierdlem104 45385 issmff 45909 issmfdf 45912 smfpimltmpt 45921 smfpimltxr 45922 smfpimltxrmptf 45933 smfpreimagtf 45943 smflim 45952 smfpimgtxr 45955 smfpimgtmpt 45956 smfpimgtxrmptf 45959 smflim2 45981 smfpimcc 45983 smfsup 45989 smfsupmpt 45990 smfsupxr 45991 smfinflem 45992 smfinf 45993 smfinfmpt 45994 smflimsup 46003 smfliminf 46006 adddmmbl2 46009 muldmmbl2 46011 smfpimne2 46015 smfdivdmmbl2 46016 fsupdm 46017 finfdm 46021 nfdfat 46294 |
Copyright terms: Public domain | W3C validator |