Theorem nfdm 5901

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 5635	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2899	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2899	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5133	. . . 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 5086  dom cdm 5625

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-dm 5635

This theorem is referenced by:  nfrn  5902  dmiin  5903  nffn  6592  nosupbnd2  27697  noinfbnd2  27712  funimass4f  32728  bnj1398  35195  bnj1491  35218  fnlimcnv  46116  fnlimfvre  46123  fnlimabslt  46128  lmbr3  46196  itgsinexplem1  46403  fourierdlem16  46572  fourierdlem21  46577  fourierdlem22  46578  fourierdlem68  46623  fourierdlem80  46635  fourierdlem103  46658  fourierdlem104  46659  issmff  47183  issmfdf  47186  smfpimltmpt  47195  smfpimltxr  47196  smfpimltxrmptf  47207  smfpreimagtf  47217  smflim  47226  smfpimgtxr  47229  smfpimgtmpt  47230  smfpimgtxrmptf  47233  smflim2  47255  smfpimcc  47257  smfsup  47263  smfsupmpt  47264  smfsupxr  47265  smfinflem  47266  smfinf  47267  smflimsup  47277  smfliminf  47280  adddmmbl2  47283  muldmmbl2  47285  smfpimne2  47289  smfdivdmmbl2  47290  fsupdm  47291  finfdm  47295  nfdfat  47590