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

Theorem nfin 4041
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 3800 . 2 (𝐴𝐵) = {𝑦𝐴𝑦𝐵}
2 nfin.2 . . . 4 𝑥𝐵
32nfcri 2929 . . 3 𝑥 𝑦𝐵
4 nfin.1 . . 3 𝑥𝐴
53, 4nfrab 3310 . 2 𝑥{𝑦𝐴𝑦𝐵}
61, 5nfcxfr 2932 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  wnfc 2919  {crab 3094  cin 3791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-in 3799
This theorem is referenced by:  csbin  4236  iunxdif3  4840  disjxun  4884  nfres  5644  nfpred  5938  cp  9051  tskwe  9109  iunconn  21640  ptclsg  21827  restmetu  22783  limciun  24095  disjunsn  29970  ordtconnlem1  30568  esum2d  30753  finminlem  32901  mbfposadd  34084  iunconnlem2  40108  inn0f  40177  disjrnmpt2  40302  disjinfi  40307  fsumiunss  40719  stoweidlem57  41205  fourierdlem80  41334  sge0iunmptlemre  41560  iundjiun  41605  pimiooltgt  41852  smflim  41916  smfpimcclem  41944  smfpimcc  41945
  Copyright terms: Public domain W3C validator