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

Theorem nfii1 4940
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 4908 . 2 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
2 nfra1 3213 . . 3 𝑥𝑥𝐴 𝑦𝐵
32nfab 2988 . 2 𝑥{𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
41, 3nfcxfr 2980 1 𝑥 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  {cab 2802  wnfc 2962  wral 3133   ciin 4906
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-iin 4908
This theorem is referenced by:  dmiin  5812  scott0  9312  gruiin  10230  iinssiin  41690  iooiinicc  42109  iooiinioc  42123  fnlimfvre  42246  fnlimabslt  42251  meaiininclem  43055  hspdifhsp  43185  smflimlem2  43335  smflim  43340  smflimmpt  43371  smfsuplem1  43372  smfsupmpt  43376  smfsupxr  43377  smfinflem  43378  smfinfmpt  43380  smflimsuplem7  43387  smflimsuplem8  43388  smflimsupmpt  43390  smfliminfmpt  43393
  Copyright terms: Public domain W3C validator