Theorem nfdm 5288

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 5048	. 2 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2		nfcv 2751	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfrn.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4		nfcv 2751	. . . . 5 ⊢ Ⅎ𝑥𝑧
5	2, 3, 4	nfbr 4629	. . . 4 ⊢ Ⅎ𝑥 𝑦𝐴𝑧
6	5	nfex 2140	. . 3 ⊢ Ⅎ𝑥∃𝑧 𝑦𝐴𝑧
7	6	nfab 2755	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
8	1, 7	nfcxfr 2749	1 ⊢ Ⅎ𝑥dom 𝐴

Syntax hints:  ∃wex 1695  {cab 2596  Ⅎwnfc 2738   class class class wbr 4583  dom cdm 5038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-dm 5048

This theorem is referenced by:  nfrn  5289  dmiin  5290  nffn  5901  funimass4f  28818  bnj1398  30356  bnj1491  30379  fnlimcnv  38734  fnlimfvre  38741  fnlimabslt  38746  itgsinexplem1  38845  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem68  39067  fourierdlem80  39079  fourierdlem103  39102  fourierdlem104  39103  issmff  39620  issmfdf  39624  smfpimltmpt  39633  smfpimltxrmpt  39645  smfpreimagtf  39654  smflim  39663  smfpimgtxr  39666  smfpimgtmpt  39667  smfpimgtxrmpt  39670  nfdfat  39859