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

Theorem nfdm 5902
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 5640 . 2 dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2 nfcv 2905 . . . . 5 𝑥𝑦
3 nfrn.1 . . . . 5 𝑥𝐴
4 nfcv 2905 . . . . 5 𝑥𝑧
52, 3, 4nfbr 5150 . . . 4 𝑥 𝑦𝐴𝑧
65nfex 2318 . . 3 𝑥𝑧 𝑦𝐴𝑧
76nfab 2911 . 2 𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
81, 7nfcxfr 2903 1 𝑥dom 𝐴
Colors of variables: wff setvar class
Syntax hints:  wex 1781  {cab 2714  wnfc 2885   class class class wbr 5103  dom cdm 5630
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-dm 5640
This theorem is referenced by:  nfrn  5903  dmiin  5904  nffn  6596  nosupbnd2  26986  noinfbnd2  27001  funimass4f  31348  bnj1398  33419  bnj1491  33442  fnlimcnv  43661  fnlimfvre  43668  fnlimabslt  43673  lmbr3  43741  itgsinexplem1  43948  fourierdlem16  44117  fourierdlem21  44122  fourierdlem22  44123  fourierdlem68  44168  fourierdlem80  44180  fourierdlem103  44203  fourierdlem104  44204  issmff  44728  issmfdf  44731  smfpimltmpt  44740  smfpimltxr  44741  smfpimltxrmptf  44752  smfpreimagtf  44762  smflim  44771  smfpimgtxr  44774  smfpimgtmpt  44775  smfpimgtxrmptf  44778  smflim2  44800  smfpimcc  44802  smfsup  44808  smfsupmpt  44809  smfsupxr  44810  smfinflem  44811  smfinf  44812  smfinfmpt  44813  smflimsup  44822  smfliminf  44825  adddmmbl2  44828  muldmmbl2  44830  smfpimne2  44834  smfdivdmmbl2  44835  fsupdm  44836  nfdfat  45108
  Copyright terms: Public domain W3C validator