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

Theorem nfdm 5903
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 5641 . 2 dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2 nfcv 2906 . . . . 5 𝑥𝑦
3 nfrn.1 . . . . 5 𝑥𝐴
4 nfcv 2906 . . . . 5 𝑥𝑧
52, 3, 4nfbr 5151 . . . 4 𝑥 𝑦𝐴𝑧
65nfex 2319 . . 3 𝑥𝑧 𝑦𝐴𝑧
76nfab 2912 . 2 𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
81, 7nfcxfr 2904 1 𝑥dom 𝐴
Colors of variables: wff setvar class
Syntax hints:  wex 1782  {cab 2715  wnfc 2886   class class class wbr 5104  dom cdm 5631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-dm 5641
This theorem is referenced by:  nfrn  5904  dmiin  5905  nffn  6597  nosupbnd2  26986  noinfbnd2  27001  funimass4f  31336  bnj1398  33407  bnj1491  33430  fnlimcnv  43630  fnlimfvre  43637  fnlimabslt  43642  lmbr3  43710  itgsinexplem1  43917  fourierdlem16  44086  fourierdlem21  44091  fourierdlem22  44092  fourierdlem68  44137  fourierdlem80  44149  fourierdlem103  44172  fourierdlem104  44173  issmff  44697  issmfdf  44700  smfpimltmpt  44709  smfpimltxr  44710  smfpimltxrmptf  44721  smfpreimagtf  44731  smflim  44740  smfpimgtxr  44743  smfpimgtmpt  44744  smfpimgtxrmptf  44747  smflim2  44769  smfpimcc  44771  smfsup  44777  smfsupmpt  44778  smfsupxr  44779  smfinflem  44780  smfinf  44781  smfinfmpt  44782  smflimsup  44791  smfliminf  44794  adddmmbl2  44797  muldmmbl2  44799  smfpimne2  44803  smfdivdmmbl2  44804  fsupdm  44805  nfdfat  45077
  Copyright terms: Public domain W3C validator