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

Theorem nfdm 5522
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 5276 . 2 dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2 nfcv 2902 . . . . 5 𝑥𝑦
3 nfrn.1 . . . . 5 𝑥𝐴
4 nfcv 2902 . . . . 5 𝑥𝑧
52, 3, 4nfbr 4851 . . . 4 𝑥 𝑦𝐴𝑧
65nfex 2301 . . 3 𝑥𝑧 𝑦𝐴𝑧
76nfab 2907 . 2 𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
81, 7nfcxfr 2900 1 𝑥dom 𝐴
Colors of variables: wff setvar class
Syntax hints:  wex 1853  {cab 2746  wnfc 2889   class class class wbr 4804  dom cdm 5266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-dm 5276
This theorem is referenced by:  nfrn  5523  dmiin  5524  nffn  6148  funimass4f  29746  bnj1398  31409  bnj1491  31432  nosupbnd2  32168  fnlimcnv  40402  fnlimfvre  40409  fnlimabslt  40414  lmbr3  40482  itgsinexplem1  40672  fourierdlem16  40843  fourierdlem21  40848  fourierdlem22  40849  fourierdlem68  40894  fourierdlem80  40906  fourierdlem103  40929  fourierdlem104  40930  issmff  41449  issmfdf  41452  smfpimltmpt  41461  smfpimltxrmpt  41473  smfpreimagtf  41482  smflim  41491  smfpimgtxr  41494  smfpimgtmpt  41495  smfpimgtxrmpt  41498  smflim2  41518  smfpimcc  41520  smfsup  41526  smfsupmpt  41527  smfsupxr  41528  smfinflem  41529  smfinf  41530  smfinfmpt  41531  smflimsup  41540  smfliminf  41543  nfdfat  41716
  Copyright terms: Public domain W3C validator