Theorem nfdm 5933

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 5661	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2923	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2923	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5152	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2355	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2929	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2921	1 ⊢ Ⅎ𝑥dom 𝐴

This proof depends on syntax axioms:  ∃wex 1812  {cab 2739  Ⅎwnfc 2908   class class class wbr 5103  dom cdm 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-dm 5661

This theorem is used by:  nfrn  5934  dmiin  5935  nffn  6638  nosupbnd2  28073  noinfbnd2  28088  funimass4f  33231  bnj1398  35664  bnj1491  35687  fnlimcnv  46676  fnlimfvre  46683  fnlimabslt  46688  lmbr3  46756  itgsinexplem1  46963  fourierdlem16  47132  fourierdlem21  47137  fourierdlem22  47138  fourierdlem68  47183  fourierdlem80  47195  fourierdlem103  47218  fourierdlem104  47219  issmff  47743  issmfdf  47746  smfpimltmpt  47755  smfpimltxr  47756  smfpimltxrmptf  47767  smfpreimagtf  47777  smflim  47786  smfpimgtxr  47789  smfpimgtmpt  47790  smfpimgtxrmptf  47793  smflim2  47815  smfpimcc  47817  smfsup  47823  smfsupmpt  47824  smfsupxr  47825  smfinflem  47826  smfinf  47827  smflimsup  47837  smfliminf  47840  adddmmbl2  47843  muldmmbl2  47845  smfpimne2  47849  smfdivdmmbl2  47850  fsupdm  47851  finfdm  47855  nfdfat  48196