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

Theorem nfun 3365
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 3191 . 2  |-  ( A  u.  B )  =  { y  |  ( y  e.  A  \/  y  e.  B ) }
2 nfun.1 . . . . 5  |-  F/_ x A
32nfcri 2446 . . . 4  |-  F/ x  y  e.  A
4 nfun.2 . . . . 5  |-  F/_ x B
54nfcri 2446 . . . 4  |-  F/ x  y  e.  B
63, 5nfor 1799 . . 3  |-  F/ x
( y  e.  A  \/  y  e.  B
)
76nfab 2456 . 2  |-  F/_ x { y  |  ( y  e.  A  \/  y  e.  B ) }
81, 7nfcxfr 2449 1  |-  F/_ x
( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    \/ wo 357    e. wcel 1701   {cab 2302   F/_wnfc 2439    u. cun 3184
This theorem is referenced by:  nfsuc  4500  nfsup  7247  iuncon  17210  esumsplit  23623  measvuni  23742  sbcung  24304  nfsymdif  24751  bnj958  28483  bnj1000  28484  bnj1408  28577  bnj1446  28586  bnj1447  28587  bnj1448  28588  bnj1466  28594  bnj1467  28595
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-un 3191
  Copyright terms: Public domain W3C validator