Theorem nfdm 5962

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 5695	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2905	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2905	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5190	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2324	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2911	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2903	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1779  {cab 2714  Ⅎwnfc 2890   class class class wbr 5143  dom cdm 5685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-dm 5695

This theorem is referenced by:  nfrn  5963  dmiin  5964  nffn  6667  nosupbnd2  27761  noinfbnd2  27776  funimass4f  32647  bnj1398  35048  bnj1491  35071  fnlimcnv  45682  fnlimfvre  45689  fnlimabslt  45694  lmbr3  45762  itgsinexplem1  45969  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem68  46189  fourierdlem80  46201  fourierdlem103  46224  fourierdlem104  46225  issmff  46749  issmfdf  46752  smfpimltmpt  46761  smfpimltxr  46762  smfpimltxrmptf  46773  smfpreimagtf  46783  smflim  46792  smfpimgtxr  46795  smfpimgtmpt  46796  smfpimgtxrmptf  46799  smflim2  46821  smfpimcc  46823  smfsup  46829  smfsupmpt  46830  smfsupxr  46831  smfinflem  46832  smfinf  46833  smflimsup  46843  smfliminf  46846  adddmmbl2  46849  muldmmbl2  46851  smfpimne2  46855  smfdivdmmbl2  46856  fsupdm  46857  finfdm  46861  nfdfat  47139