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

Theorem nfiin 4981
Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2377. See nfiing 4983 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
Hypotheses
Ref Expression
nfiun.1 𝑦𝐴
nfiun.2 𝑦𝐵
Assertion
Ref Expression
nfiin 𝑦 𝑥𝐴 𝐵
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem nfiin
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-iin 4951 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∀𝑥𝐴 𝑧𝐵}
2 nfiun.1 . . . 4 𝑦𝐴
3 nfiun.2 . . . . 5 𝑦𝐵
43nfcri 2891 . . . 4 𝑦 𝑧𝐵
52, 4nfralw 3285 . . 3 𝑦𝑥𝐴 𝑧𝐵
65nfab 2905 . 2 𝑦{𝑧 ∣ ∀𝑥𝐴 𝑧𝐵}
71, 6nfcxfr 2897 1 𝑦 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  {cab 2715  wnfc 2884  wral 3052   ciin 4949
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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-iin 4951
This theorem is referenced by:  iinab  5025  fnlimcnv  46054  fnlimfvre  46061  fnlimabslt  46066  iinhoiicc  47061  preimageiingt  47107  preimaleiinlt  47108  smflimlem6  47163  smflim  47164  smflim2  47193  smfsup  47201  smfsupmpt  47202  smfsupxr  47203  smfinflem  47204  smfinf  47205  smflimsup  47215  smfliminf  47218  fsupdm  47229  finfdm  47233
  Copyright terms: Public domain W3C validator