Theorem nfdm 5918

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 5651	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2892	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2892	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5157	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2323	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2898	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2890	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1779  {cab 2708  Ⅎwnfc 2877   class class class wbr 5110  dom cdm 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-dm 5651

This theorem is referenced by:  nfrn  5919  dmiin  5920  nffn  6620  nosupbnd2  27635  noinfbnd2  27650  funimass4f  32568  bnj1398  35031  bnj1491  35054  fnlimcnv  45672  fnlimfvre  45679  fnlimabslt  45684  lmbr3  45752  itgsinexplem1  45959  fourierdlem16  46128  fourierdlem21  46133  fourierdlem22  46134  fourierdlem68  46179  fourierdlem80  46191  fourierdlem103  46214  fourierdlem104  46215  issmff  46739  issmfdf  46742  smfpimltmpt  46751  smfpimltxr  46752  smfpimltxrmptf  46763  smfpreimagtf  46773  smflim  46782  smfpimgtxr  46785  smfpimgtmpt  46786  smfpimgtxrmptf  46789  smflim2  46811  smfpimcc  46813  smfsup  46819  smfsupmpt  46820  smfsupxr  46821  smfinflem  46822  smfinf  46823  smflimsup  46833  smfliminf  46836  adddmmbl2  46839  muldmmbl2  46841  smfpimne2  46845  smfdivdmmbl2  46846  fsupdm  46847  finfdm  46851  nfdfat  47132