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

Theorem nfun 4066
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 3868 . 2 (𝐴𝐵) = {𝑦 ∣ (𝑦𝐴𝑦𝐵)}
2 nfun.1 . . . . 5 𝑥𝐴
32nfcri 2943 . . . 4 𝑥 𝑦𝐴
4 nfun.2 . . . . 5 𝑥𝐵
54nfcri 2943 . . . 4 𝑥 𝑦𝐵
63, 5nfor 1886 . . 3 𝑥(𝑦𝐴𝑦𝐵)
76nfab 2955 . 2 𝑥{𝑦 ∣ (𝑦𝐴𝑦𝐵)}
81, 7nfcxfr 2947 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 842  wcel 2081  {cab 2775  wnfc 2933  cun 3861
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-un 3868
This theorem is referenced by:  nfsymdif  4147  csbun  4309  iunxdif3  4920  nfsuc  6142  nfsup  8766  nfdju  9187  iunconn  21725  ordtconnlem1  30789  esumsplit  30934  measvuni  31095  bnj958  31833  bnj1000  31834  bnj1408  31927  bnj1446  31936  bnj1447  31937  bnj1448  31938  bnj1466  31944  bnj1467  31945  nosupbnd2  32831  rdgssun  34215  exrecfnlem  34216  poimirlem16  34464  poimirlem19  34467  pimrecltpos  42555
  Copyright terms: Public domain W3C validator