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  43618  fnlimfvre  43625  fnlimabslt  43630  lmbr3  43698  itgsinexplem1  43905  fourierdlem16  44074  fourierdlem21  44079  fourierdlem22  44080  fourierdlem68  44125  fourierdlem80  44137  fourierdlem103  44160  fourierdlem104  44161  issmff  44683  issmfdf  44686  smfpimltmpt  44695  smfpimltxr  44696  smfpimltxrmptf  44707  smfpreimagtf  44717  smflim  44726  smfpimgtxr  44729  smfpimgtmpt  44730  smfpimgtxrmptf  44733  smflim2  44755  smfpimcc  44757  smfsup  44763  smfsupmpt  44764  smfsupxr  44765  smfinflem  44766  smfinf  44767  smfinfmpt  44768  smflimsup  44777  smfliminf  44780  adddmmbl2  44783  muldmmbl2  44785  smfpimne2  44789  smfdivdmmbl2  44790  nfdfat  45059
  Copyright terms: Public domain W3C validator