Theorem nfdm 5849

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 5590	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2906	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2906	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5117	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2322	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2912	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2904	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1783  {cab 2715  Ⅎwnfc 2886   class class class wbr 5070  dom cdm 5580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-dm 5590

This theorem is referenced by:  nfrn  5850  dmiin  5851  nffn  6516  funimass4f  30873  bnj1398  32914  bnj1491  32937  nosupbnd2  33846  noinfbnd2  33861  fnlimcnv  43098  fnlimfvre  43105  fnlimabslt  43110  lmbr3  43178  itgsinexplem1  43385  fourierdlem16  43554  fourierdlem21  43559  fourierdlem22  43560  fourierdlem68  43605  fourierdlem80  43617  fourierdlem103  43640  fourierdlem104  43641  issmff  44157  issmfdf  44160  smfpimltmpt  44169  smfpimltxrmpt  44181  smfpreimagtf  44190  smflim  44199  smfpimgtxr  44202  smfpimgtmpt  44203  smfpimgtxrmpt  44206  smflim2  44226  smfpimcc  44228  smfsup  44234  smfsupmpt  44235  smfsupxr  44236  smfinflem  44237  smfinf  44238  smfinfmpt  44239  smflimsup  44248  smfliminf  44251  nfdfat  44506