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

Theorem nfun 4072
 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 3865 . 2 (𝐴𝐵) = {𝑦 ∣ (𝑦𝐴𝑦𝐵)}
2 nfun.1 . . . . 5 𝑥𝐴
32nfcri 2906 . . . 4 𝑥 𝑦𝐴
4 nfun.2 . . . . 5 𝑥𝐵
54nfcri 2906 . . . 4 𝑥 𝑦𝐵
63, 5nfor 1905 . . 3 𝑥(𝑦𝐴𝑦𝐵)
76nfab 2925 . 2 𝑥{𝑦 ∣ (𝑦𝐴𝑦𝐵)}
81, 7nfcxfr 2917 1 𝑥(𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   ∨ wo 844   ∈ wcel 2111  {cab 2735  Ⅎwnfc 2899   ∪ cun 3858 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-un 3865 This theorem is referenced by:  nfsymdif  4153  csbun  4338  iunxdif3  4986  nfsuc  6245  nfsup  8961  nfdju  9382  iunconn  22141  ordtconnlem1  31407  esumsplit  31552  measvuni  31713  bnj958  32452  bnj1000  32453  bnj1408  32548  bnj1446  32557  bnj1447  32558  bnj1448  32559  bnj1466  32565  bnj1467  32566  nosupbnd2  33516  noinfbnd2  33531  rdgssun  35109  exrecfnlem  35110  poimirlem16  35387  poimirlem19  35390  pimrecltpos  43745
 Copyright terms: Public domain W3C validator