Theorem nfdm 5367

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 5124	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2764	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2764	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 4699	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2154	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2769	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2762	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1704  {cab 2608  Ⅎwnfc 2751   class class class wbr 4653  dom cdm 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-dm 5124

This theorem is referenced by:  nfrn  5368  dmiin  5369  nffn  5987  funimass4f  29437  bnj1398  31102  bnj1491  31125  nosupbnd2  31862  fnlimcnv  39899  fnlimfvre  39906  fnlimabslt  39911  lmbr3  39979  itgsinexplem1  40169  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem68  40391  fourierdlem80  40403  fourierdlem103  40426  fourierdlem104  40427  issmff  40943  issmfdf  40946  smfpimltmpt  40955  smfpimltxrmpt  40967  smfpreimagtf  40976  smflim  40985  smfpimgtxr  40988  smfpimgtmpt  40989  smfpimgtxrmpt  40992  smflim2  41012  smfpimcc  41014  smfsup  41020  smfsupmpt  41021  smfsupxr  41022  smfinflem  41023  smfinf  41024  smfinfmpt  41025  smflimsup  41034  smfliminf  41037  nfdfat  41210