Theorem nfdm 5893

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 5629	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2891	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2891	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5139	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2323	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2897	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2889	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1779  {cab 2707  Ⅎwnfc 2876   class class class wbr 5092  dom cdm 5619

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-dm 5629

This theorem is referenced by:  nfrn  5894  dmiin  5895  nffn  6581  nosupbnd2  27626  noinfbnd2  27641  funimass4f  32580  bnj1398  35001  bnj1491  35024  fnlimcnv  45652  fnlimfvre  45659  fnlimabslt  45664  lmbr3  45732  itgsinexplem1  45939  fourierdlem16  46108  fourierdlem21  46113  fourierdlem22  46114  fourierdlem68  46159  fourierdlem80  46171  fourierdlem103  46194  fourierdlem104  46195  issmff  46719  issmfdf  46722  smfpimltmpt  46731  smfpimltxr  46732  smfpimltxrmptf  46743  smfpreimagtf  46753  smflim  46762  smfpimgtxr  46765  smfpimgtmpt  46766  smfpimgtxrmptf  46769  smflim2  46791  smfpimcc  46793  smfsup  46799  smfsupmpt  46800  smfsupxr  46801  smfinflem  46802  smfinf  46803  smflimsup  46813  smfliminf  46816  adddmmbl2  46819  muldmmbl2  46821  smfpimne2  46825  smfdivdmmbl2  46826  fsupdm  46827  finfdm  46831  nfdfat  47115