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

Theorem nfun 3965
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 3771 . 2 (𝐴𝐵) = {𝑦 ∣ (𝑦𝐴𝑦𝐵)}
2 nfun.1 . . . . 5 𝑥𝐴
32nfcri 2941 . . . 4 𝑥 𝑦𝐴
4 nfun.2 . . . . 5 𝑥𝐵
54nfcri 2941 . . . 4 𝑥 𝑦𝐵
63, 5nfor 1999 . . 3 𝑥(𝑦𝐴𝑦𝐵)
76nfab 2952 . 2 𝑥{𝑦 ∣ (𝑦𝐴𝑦𝐵)}
81, 7nfcxfr 2945 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 865  wcel 2158  {cab 2791  wnfc 2934  cun 3764
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-un 3771
This theorem is referenced by:  nfsymdif  4043  csbun  4204  iunxdif3  4794  nfsuc  6006  nfsup  8593  nfdju  9014  iunconn  21441  ordtconnlem1  30292  esumsplit  30437  measvuni  30599  bnj958  31330  bnj1000  31331  bnj1408  31424  bnj1446  31433  bnj1447  31434  bnj1448  31435  bnj1466  31441  bnj1467  31442  nosupbnd2  32180  poimirlem16  33735  poimirlem19  33738  pimrecltpos  41398
  Copyright terms: Public domain W3C validator