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

Theorem nfun 4138
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 3938 . 2 (𝐴𝐵) = {𝑦 ∣ (𝑦𝐴𝑦𝐵)}
2 nfun.1 . . . . 5 𝑥𝐴
32nfcri 2968 . . . 4 𝑥 𝑦𝐴
4 nfun.2 . . . . 5 𝑥𝐵
54nfcri 2968 . . . 4 𝑥 𝑦𝐵
63, 5nfor 1896 . . 3 𝑥(𝑦𝐴𝑦𝐵)
76nfab 2981 . 2 𝑥{𝑦 ∣ (𝑦𝐴𝑦𝐵)}
81, 7nfcxfr 2972 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 841  wcel 2105  {cab 2796  wnfc 2958  cun 3931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-un 3938
This theorem is referenced by:  nfsymdif  4220  csbun  4387  iunxdif3  5008  nfsuc  6255  nfsup  8903  nfdju  9324  iunconn  21964  ordtconnlem1  31066  esumsplit  31211  measvuni  31372  bnj958  32111  bnj1000  32112  bnj1408  32205  bnj1446  32214  bnj1447  32215  bnj1448  32216  bnj1466  32222  bnj1467  32223  nosupbnd2  33113  rdgssun  34541  exrecfnlem  34542  poimirlem16  34789  poimirlem19  34792  pimrecltpos  42864
  Copyright terms: Public domain W3C validator