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

Theorem nfin 3650
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 3423 . 2  |-  ( A  i^i  B )  =  { y  e.  A  |  y  e.  B }
2 nfin.2 . . . 4  |-  F/_ x B
32nfcri 2596 . . 3  |-  F/ x  y  e.  B
4 nfin.1 . . 3  |-  F/_ x A
53, 4nfrab 2983 . 2  |-  F/_ x { y  e.  A  |  y  e.  B }
61, 5nfcxfr 2600 1  |-  F/_ x
( A  i^i  B
)
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1897   F/_wnfc 2589   {crab 2752    i^i cin 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rab 2757  df-in 3422
This theorem is referenced by:  csbin  3810  disjxun  4413  nfres  5125  nfpred  5403  cp  8387  tskwe  8409  iuncon  20491  ptclsg  20678  restmetu  21633  limciun  22897  iunxdif3  28223  disjunsn  28252  ordtconlem1  28778  esum2d  28962  finminlem  31022  mbfposadd  32032  csbingOLD  37254  iunconlem2  37371  inn0f  37454  disjrnmpt2  37500  disjinfi  37505  fsumiunss  37691  stoweidlem57  37955  fourierdlem80  38087  sge0iunmptlemre  38294  iundjiun  38335
  Copyright terms: Public domain W3C validator