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  45911  fnlimfvre  45918  fnlimabslt  45923  lmbr3  45991  itgsinexplem1  46198  fourierdlem16  46367  fourierdlem21  46372  fourierdlem22  46373  fourierdlem68  46418  fourierdlem80  46430  fourierdlem103  46453  fourierdlem104  46454  issmff  46978  issmfdf  46981  smfpimltmpt  46990  smfpimltxr  46991  smfpimltxrmptf  47002  smfpreimagtf  47012  smflim  47021  smfpimgtxr  47024  smfpimgtmpt  47025  smfpimgtxrmptf  47028  smflim2  47050  smfpimcc  47052  smfsup  47058  smfsupmpt  47059  smfsupxr  47060  smfinflem  47061  smfinf  47062  smflimsup  47072  smfliminf  47075  adddmmbl2  47078  muldmmbl2  47080  smfpimne2  47084  smfdivdmmbl2  47085  fsupdm  47086  finfdm  47090  nfdfat  47373