Theorem nfdm 5904

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 5641	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2891	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2891	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5149	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2323	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2897	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2889	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1779  {cab 2707  Ⅎwnfc 2876   class class class wbr 5102  dom cdm 5631

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-dm 5641

This theorem is referenced by:  nfrn  5905  dmiin  5906  nffn  6599  nosupbnd2  27661  noinfbnd2  27676  funimass4f  32611  bnj1398  35017  bnj1491  35040  fnlimcnv  45658  fnlimfvre  45665  fnlimabslt  45670  lmbr3  45738  itgsinexplem1  45945  fourierdlem16  46114  fourierdlem21  46119  fourierdlem22  46120  fourierdlem68  46165  fourierdlem80  46177  fourierdlem103  46200  fourierdlem104  46201  issmff  46725  issmfdf  46728  smfpimltmpt  46737  smfpimltxr  46738  smfpimltxrmptf  46749  smfpreimagtf  46759  smflim  46768  smfpimgtxr  46771  smfpimgtmpt  46772  smfpimgtxrmptf  46775  smflim2  46797  smfpimcc  46799  smfsup  46805  smfsupmpt  46806  smfsupxr  46807  smfinflem  46808  smfinf  46809  smflimsup  46819  smfliminf  46822  adddmmbl2  46825  muldmmbl2  46827  smfpimne2  46831  smfdivdmmbl2  46832  fsupdm  46833  finfdm  46837  nfdfat  47121