Theorem nfdm 5825

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 5567	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2979	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2979	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5115	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2343	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2986	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2977	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1780  {cab 2801  Ⅎwnfc 2963   class class class wbr 5068  dom cdm 5557

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-dm 5567

This theorem is referenced by:  nfrn  5826  dmiin  5827  nffn  6454  funimass4f  30384  bnj1398  32308  bnj1491  32331  nosupbnd2  33218  fnlimcnv  41955  fnlimfvre  41962  fnlimabslt  41967  lmbr3  42035  itgsinexplem1  42246  fourierdlem16  42415  fourierdlem21  42420  fourierdlem22  42421  fourierdlem68  42466  fourierdlem80  42478  fourierdlem103  42501  fourierdlem104  42502  issmff  43018  issmfdf  43021  smfpimltmpt  43030  smfpimltxrmpt  43042  smfpreimagtf  43051  smflim  43060  smfpimgtxr  43063  smfpimgtmpt  43064  smfpimgtxrmpt  43067  smflim2  43087  smfpimcc  43089  smfsup  43095  smfsupmpt  43096  smfsupxr  43097  smfinflem  43098  smfinf  43099  smfinfmpt  43100  smflimsup  43109  smfliminf  43112  nfdfat  43333