Theorem nfdm 5942

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 5672	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2931	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2931	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5162	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2363	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2937	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2929	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1806  {cab 2747  Ⅎwnfc 2916   class class class wbr 5113  dom cdm 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-dm 5672

This theorem is referenced by:  nfrn  5943  dmiin  5944  nffn  6635  nosupbnd2  27846  noinfbnd2  27861  funimass4f  32923  bnj1398  35367  bnj1491  35390  fnlimcnv  46273  fnlimfvre  46280  fnlimabslt  46285  lmbr3  46353  itgsinexplem1  46560  fourierdlem16  46729  fourierdlem21  46734  fourierdlem22  46735  fourierdlem68  46780  fourierdlem80  46792  fourierdlem103  46815  fourierdlem104  46816  issmff  47340  issmfdf  47343  smfpimltmpt  47352  smfpimltxr  47353  smfpimltxrmptf  47364  smfpreimagtf  47374  smflim  47383  smfpimgtxr  47386  smfpimgtmpt  47387  smfpimgtxrmptf  47390  smflim2  47412  smfpimcc  47414  smfsup  47420  smfsupmpt  47421  smfsupxr  47422  smfinflem  47423  smfinf  47424  smflimsup  47434  smfliminf  47437  adddmmbl2  47440  muldmmbl2  47442  smfpimne2  47446  smfdivdmmbl2  47447  fsupdm  47448  finfdm  47452  nfdfat  47753