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

Theorem nfii1 4743
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 4715 . 2 𝑥𝐴 𝐵 = {𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
2 nfra1 3129 . . 3 𝑥𝑥𝐴 𝑦𝐵
32nfab 2953 . 2 𝑥{𝑦 ∣ ∀𝑥𝐴 𝑦𝐵}
41, 3nfcxfr 2946 1 𝑥 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2156  {cab 2792  wnfc 2935  wral 3096   ciin 4713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-iin 4715
This theorem is referenced by:  dmiin  5570  scott0  8996  gruiin  9917  iinssiin  39803  iooiinicc  40249  iooiinioc  40263  fnlimfvre  40386  fnlimabslt  40391  meaiininclem  41182  hspdifhsp  41312  smflimlem2  41462  smflim  41467  smflimmpt  41498  smfsuplem1  41499  smfsupmpt  41503  smfsupxr  41504  smfinflem  41505  smfinfmpt  41507  smflimsuplem7  41514  smflimsuplem8  41515  smflimsupmpt  41517  smfliminfmpt  41520
  Copyright terms: Public domain W3C validator