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

Theorem nfin 3700
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 2617 . . 3  |-  F/ x  y  e.  B
4 nfin.1 . . 3  |-  F/_ x A
53, 4nfrab 3038 . 2  |-  F/_ x { y  e.  A  |  y  e.  B }
61, 5nfcxfr 2622 1  |-  F/_ x
( A  i^i  B
)
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1762   F/_wnfc 2610   {crab 2813    i^i cin 3470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rab 2818  df-in 3478
This theorem is referenced by:  csbin  3855  csbingOLD  3856  disjxun  4440  nfres  5268  cp  8300  tskwe  8322  iuncon  19690  ptclsg  19846  restmetu  20820  limciun  22028  disjunsn  27114  ordtconlem1  27530  nfpred  28814  mbfposadd  29628  finminlem  29702  stoweidlem57  31314  fourierdlem80  31444  iunconlem2  32692
  Copyright terms: Public domain W3C validator