Theorem nfdm 5900

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 5634	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2898	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2898	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5145	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2329	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2904	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2896	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1780  {cab 2714  Ⅎwnfc 2883   class class class wbr 5098  dom cdm 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-dm 5634

This theorem is referenced by:  nfrn  5901  dmiin  5902  nffn  6591  nosupbnd2  27684  noinfbnd2  27699  funimass4f  32715  bnj1398  35190  bnj1491  35213  fnlimcnv  45921  fnlimfvre  45928  fnlimabslt  45933  lmbr3  46001  itgsinexplem1  46208  fourierdlem16  46377  fourierdlem21  46382  fourierdlem22  46383  fourierdlem68  46428  fourierdlem80  46440  fourierdlem103  46463  fourierdlem104  46464  issmff  46988  issmfdf  46991  smfpimltmpt  47000  smfpimltxr  47001  smfpimltxrmptf  47012  smfpreimagtf  47022  smflim  47031  smfpimgtxr  47034  smfpimgtmpt  47035  smfpimgtxrmptf  47038  smflim2  47060  smfpimcc  47062  smfsup  47068  smfsupmpt  47069  smfsupxr  47070  smfinflem  47071  smfinf  47072  smflimsup  47082  smfliminf  47085  adddmmbl2  47088  muldmmbl2  47090  smfpimne2  47094  smfdivdmmbl2  47095  fsupdm  47096  finfdm  47100  nfdfat  47383