Theorem nfdm 5908

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 5642	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2899	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2899	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5147	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2330	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2905	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2897	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1781  {cab 2715  Ⅎwnfc 2884   class class class wbr 5100  dom cdm 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-dm 5642

This theorem is referenced by:  nfrn  5909  dmiin  5910  nffn  6599  nosupbnd2  27696  noinfbnd2  27711  funimass4f  32727  bnj1398  35210  bnj1491  35233  fnlimcnv  46025  fnlimfvre  46032  fnlimabslt  46037  lmbr3  46105  itgsinexplem1  46312  fourierdlem16  46481  fourierdlem21  46486  fourierdlem22  46487  fourierdlem68  46532  fourierdlem80  46544  fourierdlem103  46567  fourierdlem104  46568  issmff  47092  issmfdf  47095  smfpimltmpt  47104  smfpimltxr  47105  smfpimltxrmptf  47116  smfpreimagtf  47126  smflim  47135  smfpimgtxr  47138  smfpimgtmpt  47139  smfpimgtxrmptf  47142  smflim2  47164  smfpimcc  47166  smfsup  47172  smfsupmpt  47173  smfsupxr  47174  smfinflem  47175  smfinf  47176  smflimsup  47186  smfliminf  47189  adddmmbl2  47192  muldmmbl2  47194  smfpimne2  47198  smfdivdmmbl2  47199  fsupdm  47200  finfdm  47204  nfdfat  47487