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

Theorem nfdm 5568
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 5321 . 2 dom 𝐴 = {𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
2 nfcv 2948 . . . . 5 𝑥𝑦
3 nfrn.1 . . . . 5 𝑥𝐴
4 nfcv 2948 . . . . 5 𝑥𝑧
52, 3, 4nfbr 4891 . . . 4 𝑥 𝑦𝐴𝑧
65nfex 2330 . . 3 𝑥𝑧 𝑦𝐴𝑧
76nfab 2953 . 2 𝑥{𝑦 ∣ ∃𝑧 𝑦𝐴𝑧}
81, 7nfcxfr 2946 1 𝑥dom 𝐴
Colors of variables: wff setvar class
Syntax hints:  wex 1859  {cab 2792  wnfc 2935   class class class wbr 4844  dom cdm 5311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-br 4845  df-dm 5321
This theorem is referenced by:  nfrn  5569  dmiin  5570  nffn  6198  funimass4f  29764  bnj1398  31425  bnj1491  31448  nosupbnd2  32183  fnlimcnv  40379  fnlimfvre  40386  fnlimabslt  40391  lmbr3  40459  itgsinexplem1  40649  fourierdlem16  40819  fourierdlem21  40824  fourierdlem22  40825  fourierdlem68  40870  fourierdlem80  40882  fourierdlem103  40905  fourierdlem104  40906  issmff  41425  issmfdf  41428  smfpimltmpt  41437  smfpimltxrmpt  41449  smfpreimagtf  41458  smflim  41467  smfpimgtxr  41470  smfpimgtmpt  41471  smfpimgtxrmpt  41474  smflim2  41494  smfpimcc  41496  smfsup  41502  smfsupmpt  41503  smfsupxr  41504  smfinflem  41505  smfinf  41506  smfinfmpt  41507  smflimsup  41516  smfliminf  41519  nfdfat  41716
  Copyright terms: Public domain W3C validator