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

Theorem nfdm 5962
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 5695 . 2 dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2 nfcv 2905 . . . . 5 𝑥𝑦
3 nfrn.1 . . . . 5 𝑥𝐴
4 nfcv 2905 . . . . 5 𝑥𝑧
52, 3, 4nfbr 5190 . . . 4 𝑥 𝑦𝐴𝑧
65nfex 2324 . . 3 𝑥𝑧 𝑦𝐴𝑧
76nfab 2911 . 2 𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
81, 7nfcxfr 2903 1 𝑥dom 𝐴
Colors of variables: wff setvar class
Syntax hints:  wex 1779  {cab 2714  wnfc 2890   class class class wbr 5143  dom cdm 5685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-dm 5695
This theorem is referenced by:  nfrn  5963  dmiin  5964  nffn  6667  nosupbnd2  27761  noinfbnd2  27776  funimass4f  32647  bnj1398  35048  bnj1491  35071  fnlimcnv  45682  fnlimfvre  45689  fnlimabslt  45694  lmbr3  45762  itgsinexplem1  45969  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem68  46189  fourierdlem80  46201  fourierdlem103  46224  fourierdlem104  46225  issmff  46749  issmfdf  46752  smfpimltmpt  46761  smfpimltxr  46762  smfpimltxrmptf  46773  smfpreimagtf  46783  smflim  46792  smfpimgtxr  46795  smfpimgtmpt  46796  smfpimgtxrmptf  46799  smflim2  46821  smfpimcc  46823  smfsup  46829  smfsupmpt  46830  smfsupxr  46831  smfinflem  46832  smfinf  46833  smflimsup  46843  smfliminf  46846  adddmmbl2  46849  muldmmbl2  46851  smfpimne2  46855  smfdivdmmbl2  46856  fsupdm  46857  finfdm  46861  nfdfat  47139
  Copyright terms: Public domain W3C validator