Theorem nfdm 5522

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 5276	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2902	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2902	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 4851	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2301	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2907	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2900	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1853  {cab 2746  Ⅎwnfc 2889   class class class wbr 4804  dom cdm 5266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-dm 5276

This theorem is referenced by:  nfrn  5523  dmiin  5524  nffn  6148  funimass4f  29746  bnj1398  31409  bnj1491  31432  nosupbnd2  32168  fnlimcnv  40402  fnlimfvre  40409  fnlimabslt  40414  lmbr3  40482  itgsinexplem1  40672  fourierdlem16  40843  fourierdlem21  40848  fourierdlem22  40849  fourierdlem68  40894  fourierdlem80  40906  fourierdlem103  40929  fourierdlem104  40930  issmff  41449  issmfdf  41452  smfpimltmpt  41461  smfpimltxrmpt  41473  smfpreimagtf  41482  smflim  41491  smfpimgtxr  41494  smfpimgtmpt  41495  smfpimgtxrmpt  41498  smflim2  41518  smfpimcc  41520  smfsup  41526  smfsupmpt  41527  smfsupxr  41528  smfinflem  41529  smfinf  41530  smfinfmpt  41531  smflimsup  41540  smfliminf  41543  nfdfat  41716