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

Theorem nfdm 5271
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 5034 . 2 dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2 nfcv 2746 . . . . 5 𝑥𝑦
3 nfrn.1 . . . . 5 𝑥𝐴
4 nfcv 2746 . . . . 5 𝑥𝑧
52, 3, 4nfbr 4619 . . . 4 𝑥 𝑦𝐴𝑧
65nfex 2137 . . 3 𝑥𝑧 𝑦𝐴𝑧
76nfab 2750 . 2 𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
81, 7nfcxfr 2744 1 𝑥dom 𝐴
Colors of variables: wff setvar class
Syntax hints:  wex 1694  {cab 2591  wnfc 2733   class class class wbr 4573  dom cdm 5024
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-br 4574  df-dm 5034
This theorem is referenced by:  nfrn  5272  dmiin  5273  nffn  5883  funimass4f  28620  bnj1398  30158  bnj1491  30181  fnlimcnv  38534  fnlimfvre  38541  fnlimabslt  38546  itgsinexplem1  38645  fourierdlem16  38816  fourierdlem21  38821  fourierdlem22  38822  fourierdlem68  38867  fourierdlem80  38879  fourierdlem103  38902  fourierdlem104  38903  issmff  39420  issmfdf  39424  smfpimltmpt  39433  smfpimltxrmpt  39445  smfpreimagtf  39454  smflim  39463  smfpimgtxr  39466  smfpimgtmpt  39467  smfpimgtxrmpt  39470  nfdfat  39660
  Copyright terms: Public domain W3C validator