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

Theorem nfii1 4522
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 4493 . 2 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
2 nfra1 2941 . . 3 𝑥𝑥𝐴 𝑦𝐵
32nfab 2771 . 2 𝑥{𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
41, 3nfcxfr 2765 1 𝑥 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 1992  {cab 2612  wnfc 2754  wral 2912   ciin 4491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-iin 4493
This theorem is referenced by:  dmiin  5333  scott0  8694  gruiin  9577  iinssiin  38786  iooiinicc  39167  iooiinioc  39181  fnlimfvre  39297  fnlimabslt  39302  meaiininclem  39994  hspdifhsp  40124  smflimlem2  40274  smflim  40279  smflimmpt  40310  smfsuplem1  40311  smfsupmpt  40315  smfsupxr  40316  smfinflem  40317  smfinfmpt  40319  smflimsuplem7  40326  smflimsuplem8  40327  smflimsupmpt  40329
  Copyright terms: Public domain W3C validator