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

Theorem nfii1 4987
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 4954 . 2 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
2 nfra1 3286 . . 3 𝑥𝑥𝐴 𝑦𝐵
32nfab 2928 . 2 𝑥{𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
41, 3nfcxfr 2920 1 𝑥 𝑥𝐴 𝐵
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wcel 2145  {cab 2738  wnfc 2907  wral 3076   ciin 4952
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-iin 4954
This theorem is used by:  dmiin  5939  scott0b  9901  scott0OLD  9902  gruiin  10844  zarclsiin  34414  iinssiin  46026  iooiinicc  46437  iooiinioc  46451  fnlimfvre  46567  fnlimabslt  46572  meaiininclem  47379  hspdifhsp  47509  smflimlem2  47665  smflim  47670  smflimmpt  47703  smfsuplem1  47704  smfsupmpt  47708  smfsupxr  47709  smfinflem  47710  smfinfmpt  47712  smflimsuplem7  47719  smflimsuplem8  47720  smflimsupmpt  47722  smfliminfmpt  47725  fsupdm  47735  finfdm  47739  iinfssc  50048  iinfsubc  50049
  Copyright terms: Public domain W3C validator