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

Theorem nfdm 5356
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 5114 . 2 dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2 nfcv 2762 . . . . 5 𝑥𝑦
3 nfrn.1 . . . . 5 𝑥𝐴
4 nfcv 2762 . . . . 5 𝑥𝑧
52, 3, 4nfbr 4690 . . . 4 𝑥 𝑦𝐴𝑧
65nfex 2152 . . 3 𝑥𝑧 𝑦𝐴𝑧
76nfab 2766 . 2 𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
81, 7nfcxfr 2760 1 𝑥dom 𝐴
Colors of variables: wff setvar class
Syntax hints:  wex 1702  {cab 2606  wnfc 2749   class class class wbr 4644  dom cdm 5104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-dm 5114
This theorem is referenced by:  nfrn  5357  dmiin  5358  nffn  5975  funimass4f  29410  bnj1398  31076  bnj1491  31099  nosupbnd2  31836  fnlimcnv  39699  fnlimfvre  39706  fnlimabslt  39711  itgsinexplem1  39932  fourierdlem16  40103  fourierdlem21  40108  fourierdlem22  40109  fourierdlem68  40154  fourierdlem80  40166  fourierdlem103  40189  fourierdlem104  40190  issmff  40706  issmfdf  40709  smfpimltmpt  40718  smfpimltxrmpt  40730  smfpreimagtf  40739  smflim  40748  smfpimgtxr  40751  smfpimgtmpt  40752  smfpimgtxrmpt  40755  smflim2  40775  smfpimcc  40777  smfsup  40783  smfsupmpt  40784  smfsupxr  40785  smfinflem  40786  smfinf  40787  smfinfmpt  40788  smflimsup  40797  smfliminf  40800  nfdfat  40973
  Copyright terms: Public domain W3C validator