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

Theorem nfii1 4825
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 4796 . 2 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
2 nfra1 3169 . . 3 𝑥𝑥𝐴 𝑦𝐵
32nfab 2938 . 2 𝑥{𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
41, 3nfcxfr 2930 1 𝑥 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2050  {cab 2758  wnfc 2916  wral 3088   ciin 4794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-iin 4796
This theorem is referenced by:  dmiin  5669  scott0  9111  gruiin  10032  iinssiin  40818  iooiinicc  41250  iooiinioc  41264  fnlimfvre  41387  fnlimabslt  41392  meaiininclem  42200  hspdifhsp  42330  smflimlem2  42480  smflim  42485  smflimmpt  42516  smfsuplem1  42517  smfsupmpt  42521  smfsupxr  42522  smfinflem  42523  smfinfmpt  42525  smflimsuplem7  42532  smflimsuplem8  42533  smflimsupmpt  42535  smfliminfmpt  42538
  Copyright terms: Public domain W3C validator