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

Theorem nfiin 4935
Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2371. See nfiing 4937 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 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 4907 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∀𝑥𝐴 𝑧𝐵}
2 nfiun.1 . . . 4 𝑦𝐴
3 nfiun.2 . . . . 5 𝑦𝐵
43nfcri 2891 . . . 4 𝑦 𝑧𝐵
52, 4nfralw 3147 . . 3 𝑦𝑥𝐴 𝑧𝐵
65nfab 2910 . 2 𝑦{𝑧 ∣ ∀𝑥𝐴 𝑧𝐵}
71, 6nfcxfr 2902 1 𝑦 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2110  {cab 2714  wnfc 2884  wral 3061   ciin 4905
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-iin 4907
This theorem is referenced by:  iinab  4976  fnlimcnv  42883  fnlimfvre  42890  fnlimabslt  42895  iinhoiicc  43887  preimageiingt  43929  preimaleiinlt  43930  smflimlem6  43983  smflim  43984  smflim2  44011  smfsup  44019  smfsupmpt  44020  smfsupxr  44021  smfinflem  44022  smfinf  44023  smfinfmpt  44024  smflimsup  44033  smfliminf  44036
  Copyright terms: Public domain W3C validator