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

Theorem nfun 3912
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 3720 . 2 (𝐴𝐵) = {𝑦 ∣ (𝑦𝐴𝑦𝐵)}
2 nfun.1 . . . . 5 𝑥𝐴
32nfcri 2896 . . . 4 𝑥 𝑦𝐴
4 nfun.2 . . . . 5 𝑥𝐵
54nfcri 2896 . . . 4 𝑥 𝑦𝐵
63, 5nfor 1983 . . 3 𝑥(𝑦𝐴𝑦𝐵)
76nfab 2907 . 2 𝑥{𝑦 ∣ (𝑦𝐴𝑦𝐵)}
81, 7nfcxfr 2900 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 382  wcel 2139  {cab 2746  wnfc 2889  cun 3713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-un 3720
This theorem is referenced by:  nfsymdif  3991  csbun  4152  iunxdif3  4758  nfsuc  5957  nfsup  8524  nfdju  8945  iunconn  21453  ordtconnlem1  30300  esumsplit  30445  measvuni  30607  bnj958  31338  bnj1000  31339  bnj1408  31432  bnj1446  31441  bnj1447  31442  bnj1448  31443  bnj1466  31449  bnj1467  31450  nosupbnd2  32189  poimirlem16  33756  poimirlem19  33759  pimrecltpos  41443
  Copyright terms: Public domain W3C validator