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

Theorem nfun 4157
Description: Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.)
Hypotheses
Ref Expression
nfun.1 𝑥𝐴
nfun.2 𝑥𝐵
Assertion
Ref Expression
nfun 𝑥(𝐴𝐵)

Proof of Theorem nfun
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-un 3945 . 2 (𝐴𝐵) = {𝑦 ∣ (𝑦𝐴𝑦𝐵)}
2 nfun.1 . . . . 5 𝑥𝐴
32nfcri 2882 . . . 4 𝑥 𝑦𝐴
4 nfun.2 . . . . 5 𝑥𝐵
54nfcri 2882 . . . 4 𝑥 𝑦𝐵
63, 5nfor 1899 . . 3 𝑥(𝑦𝐴𝑦𝐵)
76nfab 2901 . 2 𝑥{𝑦 ∣ (𝑦𝐴𝑦𝐵)}
81, 7nfcxfr 2893 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 844  wcel 2098  {cab 2701  wnfc 2875  cun 3938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-un 3945
This theorem is referenced by:  nfsymdif  4238  csbun  4430  iunxdif3  5088  nfsuc  6426  nfsup  9441  nfdju  9897  iunconn  23242  nosupbnd2  27553  noinfbnd2  27568  ordtconnlem1  33359  esumsplit  33506  measvuni  33667  bnj958  34406  bnj1000  34407  bnj1408  34502  bnj1446  34511  bnj1447  34512  bnj1448  34513  bnj1466  34519  bnj1467  34520  rdgssun  36715  exrecfnlem  36716  poimirlem16  36960  poimirlem19  36963  pimxrneun  44650  pimrecltpos  45875
  Copyright terms: Public domain W3C validator