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

Theorem nfin 4171
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 3921 . 2 (𝐴𝐵) = {𝑦𝐴𝑦𝐵}
2 nfin.2 . . . 4 𝑥𝐵
32nfcri 2967 . . 3 𝑥 𝑦𝐵
4 nfin.1 . . 3 𝑥𝐴
53, 4nfrabw 3372 . 2 𝑥{𝑦𝐴𝑦𝐵}
61, 5nfcxfr 2971 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  wnfc 2957  {crab 3129  cin 3912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-rab 3134  df-in 3920
This theorem is referenced by:  csbin  4367  iunxdif3  4993  disjxun  5040  nfres  5831  nfpred  6129  cp  9298  tskwe  9357  iunconn  22012  ptclsg  22199  restmetu  23156  limciun  24476  disjunsn  30331  ordtconnlem1  31175  esum2d  31360  finminlem  33674  bj-rcleqf  34354  mbfposadd  34980  iunconnlem2  41424  inn0f  41490  disjrnmpt2  41603  disjinfi  41608  fsumiunss  42008  stoweidlem57  42490  fourierdlem80  42619  sge0iunmptlemre  42845  iundjiun  42890  pimiooltgt  43137  smflim  43201  smfpimcclem  43229  smfpimcc  43230
  Copyright terms: Public domain W3C validator