Theorem nfdm 5935

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 5665	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2922	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2922	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5152	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2354	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2928	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2920	1 ⊢ Ⅎ𝑥dom 𝐴

This proof depends on syntax axioms:  ∃wex 1812  {cab 2738  Ⅎwnfc 2907   class class class wbr 5103  dom cdm 5655

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413  df-v 3452  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 5665

This theorem is used by:  nfrn  5936  dmiin  5937  nffn  6632  nosupbnd2  27953  noinfbnd2  27968  funimass4f  33111  bnj1398  35544  bnj1491  35567  fnlimcnv  46496  fnlimfvre  46503  fnlimabslt  46508  lmbr3  46576  itgsinexplem1  46783  fourierdlem16  46952  fourierdlem21  46957  fourierdlem22  46958  fourierdlem68  47003  fourierdlem80  47015  fourierdlem103  47038  fourierdlem104  47039  issmff  47563  issmfdf  47566  smfpimltmpt  47575  smfpimltxr  47576  smfpimltxrmptf  47587  smfpreimagtf  47597  smflim  47606  smfpimgtxr  47609  smfpimgtmpt  47610  smfpimgtxrmptf  47613  smflim2  47635  smfpimcc  47637  smfsup  47643  smfsupmpt  47644  smfsupxr  47645  smfinflem  47646  smfinf  47647  smflimsup  47657  smfliminf  47660  adddmmbl2  47663  muldmmbl2  47665  smfpimne2  47669  smfdivdmmbl2  47670  fsupdm  47671  finfdm  47675  nfdfat  48016