nfdm - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nfdm		Structured version Visualization version GIF version

Theorem nfdm 5953

Description: Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)

**Hypothesis**
Ref	Expression
nfrn.1	⊢ Ⅎ𝑥𝐴

**Assertion**
Ref	Expression
nfdm	⊢ Ⅎ𝑥dom 𝐴

Proof of Theorem nfdm Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-dm 5688	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2899	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2899	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5195	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2313	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2905	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2897	1 ⊢ Ⅎ𝑥dom 𝐴

Colors of variables: wff setvar class

Syntax hints: ∃wex 1774 {cab 2705 Ⅎwnfc 2879 class class class wbr 5148 dom cdm 5678

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-rab 3430 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5149 df-dm 5688

This theorem is referenced by: nfrn 5954 dmiin 5955 nffn 6653 nosupbnd2 27648 noinfbnd2 27663 funimass4f 32421 bnj1398 34665 bnj1491 34688 fnlimcnv 45055 fnlimfvre 45062 fnlimabslt 45067 lmbr3 45135 itgsinexplem1 45342 fourierdlem16 45511 fourierdlem21 45516 fourierdlem22 45517 fourierdlem68 45562 fourierdlem80 45574 fourierdlem103 45597 fourierdlem104 45598 issmff 46122 issmfdf 46125 smfpimltmpt 46134 smfpimltxr 46135 smfpimltxrmptf 46146 smfpreimagtf 46156 smflim 46165 smfpimgtxr 46168 smfpimgtmpt 46169 smfpimgtxrmptf 46172 smflim2 46194 smfpimcc 46196 smfsup 46202 smfsupmpt 46203 smfsupxr 46204 smfinflem 46205 smfinf 46206 smfinfmpt 46207 smflimsup 46216 smfliminf 46219 adddmmbl2 46222 muldmmbl2 46224 smfpimne2 46228 smfdivdmmbl2 46229 fsupdm 46230 finfdm 46234 nfdfat 46507

	
		OSZAR »