Theorem nfdm 5860

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 5599	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2907	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2907	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5121	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2318	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2913	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2905	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1782  {cab 2715  Ⅎwnfc 2887   class class class wbr 5074  dom cdm 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-dm 5599

This theorem is referenced by:  nfrn  5861  dmiin  5862  nffn  6532  funimass4f  30972  bnj1398  33014  bnj1491  33037  nosupbnd2  33919  noinfbnd2  33934  fnlimcnv  43208  fnlimfvre  43215  fnlimabslt  43220  lmbr3  43288  itgsinexplem1  43495  fourierdlem16  43664  fourierdlem21  43669  fourierdlem22  43670  fourierdlem68  43715  fourierdlem80  43727  fourierdlem103  43750  fourierdlem104  43751  issmff  44270  issmfdf  44273  smfpimltmpt  44282  smfpimltxr  44283  smfpimltxrmpt  44294  smfpreimagtf  44303  smflim  44312  smfpimgtxr  44315  smfpimgtmpt  44316  smfpimgtxrmpt  44319  smflim2  44339  smfpimcc  44341  smfsup  44347  smfsupmpt  44348  smfsupxr  44349  smfinflem  44350  smfinf  44351  smfinfmpt  44352  smflimsup  44361  smfliminf  44364  nfdfat  44619