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

Theorem nfin 4190
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 3941 . 2 (𝐴𝐵) = {𝑦𝐴𝑦𝐵}
2 nfin.2 . . . 4 𝑥𝐵
32nfcri 2968 . . 3 𝑥 𝑦𝐵
4 nfin.1 . . 3 𝑥𝐴
53, 4nfrabw 3383 . 2 𝑥{𝑦𝐴𝑦𝐵}
61, 5nfcxfr 2972 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  wnfc 2958  {crab 3139  cin 3932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-in 3940
This theorem is referenced by:  csbin  4388  iunxdif3  5008  disjxun  5055  nfres  5848  nfpred  6146  cp  9308  tskwe  9367  iunconn  21964  ptclsg  22151  restmetu  23107  limciun  24419  disjunsn  30272  ordtconnlem1  31066  esum2d  31251  finminlem  33563  bj-rcleqf  34234  mbfposadd  34820  iunconnlem2  41146  inn0f  41212  disjrnmpt2  41325  disjinfi  41330  fsumiunss  41732  stoweidlem57  42219  fourierdlem80  42348  sge0iunmptlemre  42574  iundjiun  42619  pimiooltgt  42866  smflim  42930  smfpimcclem  42958  smfpimcc  42959
  Copyright terms: Public domain W3C validator