Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfdm Structured version   Visualization version   GIF version

Theorem nfdm 5791
 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.
StepHypRef Expression
1 df-dm 5533 . 2 dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2 nfcv 2955 . . . . 5 𝑥𝑦
3 nfrn.1 . . . . 5 𝑥𝐴
4 nfcv 2955 . . . . 5 𝑥𝑧
52, 3, 4nfbr 5081 . . . 4 𝑥 𝑦𝐴𝑧
65nfex 2332 . . 3 𝑥𝑧 𝑦𝐴𝑧
76nfab 2961 . 2 𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
81, 7nfcxfr 2953 1 𝑥dom 𝐴
 Colors of variables: wff setvar class Syntax hints:  ∃wex 1781  {cab 2776  Ⅎwnfc 2936   class class class wbr 5034  dom cdm 5523 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3444  df-dif 3886  df-un 3888  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5035  df-dm 5533 This theorem is referenced by:  nfrn  5792  dmiin  5793  nffn  6430  funimass4f  30440  bnj1398  32482  bnj1491  32505  nosupbnd2  33406  noinfbnd2  33421  fnlimcnv  42477  fnlimfvre  42484  fnlimabslt  42489  lmbr3  42557  itgsinexplem1  42764  fourierdlem16  42933  fourierdlem21  42938  fourierdlem22  42939  fourierdlem68  42984  fourierdlem80  42996  fourierdlem103  43019  fourierdlem104  43020  issmff  43536  issmfdf  43539  smfpimltmpt  43548  smfpimltxrmpt  43560  smfpreimagtf  43569  smflim  43578  smfpimgtxr  43581  smfpimgtmpt  43582  smfpimgtxrmpt  43585  smflim2  43605  smfpimcc  43607  smfsup  43613  smfsupmpt  43614  smfsupxr  43615  smfinflem  43616  smfinf  43617  smfinfmpt  43618  smflimsup  43627  smfliminf  43630  nfdfat  43851
 Copyright terms: Public domain W3C validator