Theorem nfdm 5898

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 5632	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2896	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2896	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5143	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2327	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2902	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2894	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1780  {cab 2712  Ⅎwnfc 2881   class class class wbr 5096  dom cdm 5622

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-dm 5632

This theorem is referenced by:  nfrn  5899  dmiin  5900  nffn  6589  nosupbnd2  27682  noinfbnd2  27697  funimass4f  32664  bnj1398  35139  bnj1491  35162  fnlimcnv  45853  fnlimfvre  45860  fnlimabslt  45865  lmbr3  45933  itgsinexplem1  46140  fourierdlem16  46309  fourierdlem21  46314  fourierdlem22  46315  fourierdlem68  46360  fourierdlem80  46372  fourierdlem103  46395  fourierdlem104  46396  issmff  46920  issmfdf  46923  smfpimltmpt  46932  smfpimltxr  46933  smfpimltxrmptf  46944  smfpreimagtf  46954  smflim  46963  smfpimgtxr  46966  smfpimgtmpt  46967  smfpimgtxrmptf  46970  smflim2  46992  smfpimcc  46994  smfsup  47000  smfsupmpt  47001  smfsupxr  47002  smfinflem  47003  smfinf  47004  smflimsup  47014  smfliminf  47017  adddmmbl2  47020  muldmmbl2  47022  smfpimne2  47026  smfdivdmmbl2  47027  fsupdm  47028  finfdm  47032  nfdfat  47315