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

Theorem nfii1 4989
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 4957 . 2 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
2 nfra1 3267 . . 3 𝑥𝑥𝐴 𝑦𝐵
32nfab 2913 . 2 𝑥{𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
41, 3nfcxfr 2905 1 𝑥 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  {cab 2713  wnfc 2887  wral 3064   ciin 4955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ral 3065  df-iin 4957
This theorem is referenced by:  dmiin  5908  scott0  9822  gruiin  10746  zarclsiin  32452  iinssiin  43329  iooiinicc  43770  iooiinioc  43784  fnlimfvre  43905  fnlimabslt  43910  meaiininclem  44717  hspdifhsp  44847  smflimlem2  45003  smflim  45008  smflimmpt  45041  smfsuplem1  45042  smfsupmpt  45046  smfsupxr  45047  smfinflem  45048  smfinfmpt  45050  smflimsuplem7  45057  smflimsuplem8  45058  smflimsupmpt  45060  smfliminfmpt  45063  fsupdm  45073  finfdm  45077
  Copyright terms: Public domain W3C validator