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

Theorem nfun 3628
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  |-  F/_ x A
nfun.2  |-  F/_ x B
Assertion
Ref Expression
nfun  |-  F/_ x
( A  u.  B
)

Proof of Theorem nfun
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-un 3447 . 2  |-  ( A  u.  B )  =  { y  |  ( y  e.  A  \/  y  e.  B ) }
2 nfun.1 . . . . 5  |-  F/_ x A
32nfcri 2584 . . . 4  |-  F/ x  y  e.  A
4 nfun.2 . . . . 5  |-  F/_ x B
54nfcri 2584 . . . 4  |-  F/ x  y  e.  B
63, 5nfor 1993 . . 3  |-  F/ x
( y  e.  A  \/  y  e.  B
)
76nfab 2595 . 2  |-  F/_ x { y  |  ( y  e.  A  \/  y  e.  B ) }
81, 7nfcxfr 2589 1  |-  F/_ x
( A  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 369    e. wcel 1870   {cab 2414   F/_wnfc 2577    u. cun 3440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-un 3447
This theorem is referenced by:  nfsymdif  3703  csbun  3832  nfsuc  5513  nfsup  7971  iuncon  20374  iunxdif3  28014  ordtconlem1  28569  esumsplit  28713  measvuni  28875  bnj958  29539  bnj1000  29540  bnj1408  29633  bnj1446  29642  bnj1447  29643  bnj1448  29644  bnj1466  29650  bnj1467  29651  poimirlem16  31663  poimirlem19  31666
  Copyright terms: Public domain W3C validator