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

Theorem nfii1 5034
Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.)
Assertion
Ref Expression
nfii1 𝑥 𝑥𝐴 𝐵

Proof of Theorem nfii1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-iin 4999 . 2 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
2 nfra1 3282 . . 3 𝑥𝑥𝐴 𝑦𝐵
32nfab 2909 . 2 𝑥{𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
41, 3nfcxfr 2901 1 𝑥 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  {cab 2712  wnfc 2888  wral 3059   ciin 4997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-iin 4999
This theorem is referenced by:  dmiin  5967  scott0  9924  gruiin  10848  zarclsiin  33832  iinssiin  45069  iooiinicc  45495  iooiinioc  45509  fnlimfvre  45630  fnlimabslt  45635  meaiininclem  46442  hspdifhsp  46572  smflimlem2  46728  smflim  46733  smflimmpt  46766  smfsuplem1  46767  smfsupmpt  46771  smfsupxr  46772  smfinflem  46773  smfinfmpt  46775  smflimsuplem7  46782  smflimsuplem8  46783  smflimsupmpt  46785  smfliminfmpt  46788  fsupdm  46798  finfdm  46802
  Copyright terms: Public domain W3C validator