Theorem nfdm 5941

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 5671	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2925	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2925	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 5158	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2357	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2931	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2923	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1809  {cab 2741  Ⅎwnfc 2910   class class class wbr 5109  dom cdm 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-dm 5671

This theorem is referenced by:  nfrn  5942  dmiin  5943  nffn  6634  nosupbnd2  27880  noinfbnd2  27895  funimass4f  32982  bnj1398  35422  bnj1491  35445  fnlimcnv  46401  fnlimfvre  46408  fnlimabslt  46413  lmbr3  46481  itgsinexplem1  46688  fourierdlem16  46857  fourierdlem21  46862  fourierdlem22  46863  fourierdlem68  46908  fourierdlem80  46920  fourierdlem103  46943  fourierdlem104  46944  issmff  47468  issmfdf  47471  smfpimltmpt  47480  smfpimltxr  47481  smfpimltxrmptf  47492  smfpreimagtf  47502  smflim  47511  smfpimgtxr  47514  smfpimgtmpt  47515  smfpimgtxrmptf  47518  smflim2  47540  smfpimcc  47542  smfsup  47548  smfsupmpt  47549  smfsupxr  47550  smfinflem  47551  smfinf  47552  smflimsup  47562  smfliminf  47565  adddmmbl2  47568  muldmmbl2  47570  smfpimne2  47574  smfdivdmmbl2  47575  fsupdm  47576  finfdm  47580  nfdfat  47884