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

Theorem nfin 3545
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 3324 . 2  |-  ( A  i^i  B )  =  { y  e.  A  |  y  e.  B }
2 nfin.2 . . . 4  |-  F/_ x B
32nfcri 2563 . . 3  |-  F/ x  y  e.  B
4 nfin.1 . . 3  |-  F/_ x A
53, 4nfrab 2892 . 2  |-  F/_ x { y  e.  A  |  y  e.  B }
61, 5nfcxfr 2566 1  |-  F/_ x
( A  i^i  B
)
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755   F/_wnfc 2556   {crab 2709    i^i cin 3315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-in 3323
This theorem is referenced by:  csbin  3700  csbingOLD  3701  disjxun  4278  nfres  5099  cp  8086  tskwe  8108  iuncon  18873  ptclsg  19029  restmetu  20003  limciun  21210  disjunsn  25759  ordtconlem1  26207  nfpred  27476  mbfposadd  28280  finminlem  28354  stoweidlem57  29695  iunconlem2  31370
  Copyright terms: Public domain W3C validator