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 5628	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2901	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2901	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5119	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2333	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2907	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2899	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1786  {cab 2717  Ⅎwnfc 2886   class class class wbr 5072  dom cdm 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-dm 5628

This theorem is referenced by:  nfrn  5894  dmiin  5895  nffn  6584  nosupbnd2  27698  noinfbnd2  27713  funimass4f  32729  bnj1398  35216  bnj1491  35239  fnlimcnv  46110  fnlimfvre  46117  fnlimabslt  46122  lmbr3  46190  itgsinexplem1  46397  fourierdlem16  46566  fourierdlem21  46571  fourierdlem22  46572  fourierdlem68  46617  fourierdlem80  46629  fourierdlem103  46652  fourierdlem104  46653  issmff  47177  issmfdf  47180  smfpimltmpt  47189  smfpimltxr  47190  smfpimltxrmptf  47201  smfpreimagtf  47211  smflim  47220  smfpimgtxr  47223  smfpimgtmpt  47224  smfpimgtxrmptf  47227  smflim2  47249  smfpimcc  47251  smfsup  47257  smfsupmpt  47258  smfsupxr  47259  smfinflem  47260  smfinf  47261  smflimsup  47271  smfliminf  47274  adddmmbl2  47277  muldmmbl2  47279  smfpimne2  47283  smfdivdmmbl2  47284  fsupdm  47285  finfdm  47289  nfdfat  47590