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

Theorem nfin 3853
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 𝑥𝐴
nfin.2 𝑥𝐵
Assertion
Ref Expression
nfin 𝑥(𝐴𝐵)

Proof of Theorem nfin
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dfin5 3615 . 2 (𝐴𝐵) = {𝑦𝐴𝑦𝐵}
2 nfin.2 . . . 4 𝑥𝐵
32nfcri 2787 . . 3 𝑥 𝑦𝐵
4 nfin.1 . . 3 𝑥𝐴
53, 4nfrab 3153 . 2 𝑥{𝑦𝐴𝑦𝐵}
61, 5nfcxfr 2791 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  wnfc 2780  {crab 2945  cin 3606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-in 3614
This theorem is referenced by:  csbin  4043  iunxdif3  4638  disjxun  4683  nfres  5430  nfpred  5723  cp  8792  tskwe  8814  iunconn  21279  ptclsg  21466  restmetu  22422  limciun  23703  disjunsn  29533  ordtconnlem1  30098  esum2d  30283  finminlem  32437  mbfposadd  33587  csbingOLD  39369  iunconnlem2  39485  inn0f  39556  disjrnmpt2  39689  disjinfi  39694  fsumiunss  40125  stoweidlem57  40592  fourierdlem80  40721  sge0iunmptlemre  40950  iundjiun  40995  pimiooltgt  41242  smflim  41306  smfpimcclem  41334  smfpimcc  41335
  Copyright terms: Public domain W3C validator