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

Theorem nfin 3701
Description: Bound-variable hypothesis builder for the intersection of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.)
Hypotheses
Ref Expression
nfin.1  |-  F/_ x A
nfin.2  |-  F/_ x B
Assertion
Ref Expression
nfin  |-  F/_ x
( A  i^i  B
)

Proof of Theorem nfin
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dfin5 3479 . 2  |-  ( A  i^i  B )  =  { y  e.  A  |  y  e.  B }
2 nfin.2 . . . 4  |-  F/_ x B
32nfcri 2612 . . 3  |-  F/ x  y  e.  B
4 nfin.1 . . 3  |-  F/_ x A
53, 4nfrab 3039 . 2  |-  F/_ x { y  e.  A  |  y  e.  B }
61, 5nfcxfr 2617 1  |-  F/_ x
( A  i^i  B
)
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1819   F/_wnfc 2605   {crab 2811    i^i cin 3470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-in 3478
This theorem is referenced by:  csbin  3863  csbingOLD  3864  disjxun  4454  nfres  5285  cp  8326  tskwe  8348  iuncon  20054  ptclsg  20241  restmetu  21215  limciun  22423  iunxdif3  27564  disjunsn  27590  ordtconlem1  28059  esum2d  28253  nfpred  29423  mbfposadd  30224  finminlem  30298  stoweidlem57  32000  fourierdlem80  32130  iunconlem2  33836
  Copyright terms: Public domain W3C validator