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

Theorem nfin 3578
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 3357 . 2  |-  ( A  i^i  B )  =  { y  e.  A  |  y  e.  B }
2 nfin.2 . . . 4  |-  F/_ x B
32nfcri 2582 . . 3  |-  F/ x  y  e.  B
4 nfin.1 . . 3  |-  F/_ x A
53, 4nfrab 2923 . 2  |-  F/_ x { y  e.  A  |  y  e.  B }
61, 5nfcxfr 2587 1  |-  F/_ x
( A  i^i  B
)
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   F/_wnfc 2575   {crab 2740    i^i cin 3348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2745  df-in 3356
This theorem is referenced by:  csbin  3733  csbingOLD  3734  disjxun  4311  nfres  5133  cp  8119  tskwe  8141  iuncon  19054  ptclsg  19210  restmetu  20184  limciun  21391  disjunsn  25958  ordtconlem1  26376  nfpred  27652  mbfposadd  28465  finminlem  28539  stoweidlem57  29878  iunconlem2  31767
  Copyright terms: Public domain W3C validator