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

Theorem nfiin 5022
Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2366. See nfiing 5024 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 4994 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∀𝑥𝐴 𝑧𝐵}
2 nfiun.1 . . . 4 𝑦𝐴
3 nfiun.2 . . . . 5 𝑦𝐵
43nfcri 2885 . . . 4 𝑦 𝑧𝐵
52, 4nfralw 3303 . . 3 𝑦𝑥𝐴 𝑧𝐵
65nfab 2904 . 2 𝑦{𝑧 ∣ ∀𝑥𝐴 𝑧𝐵}
71, 6nfcxfr 2896 1 𝑦 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2099  {cab 2704  wnfc 2878  wral 3056   ciin 4992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ral 3057  df-iin 4994
This theorem is referenced by:  iinab  5065  fnlimcnv  44978  fnlimfvre  44985  fnlimabslt  44990  iinhoiicc  45985  preimageiingt  46031  preimaleiinlt  46032  smflimlem6  46087  smflim  46088  smflim2  46117  smfsup  46125  smfsupmpt  46126  smfsupxr  46127  smfinflem  46128  smfinf  46129  smfinfmpt  46130  smflimsup  46139  smfliminf  46142  fsupdm  46153  finfdm  46157
  Copyright terms: Public domain W3C validator