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

Theorem nfiin 4913
 Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2379. See nfiing 4915 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 4885 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∀𝑥𝐴 𝑧𝐵}
2 nfiun.1 . . . 4 𝑦𝐴
3 nfiun.2 . . . . 5 𝑦𝐵
43nfcri 2943 . . . 4 𝑦 𝑧𝐵
52, 4nfralw 3189 . . 3 𝑦𝑥𝐴 𝑧𝐵
65nfab 2961 . 2 𝑦{𝑧 ∣ ∀𝑥𝐴 𝑧𝐵}
71, 6nfcxfr 2953 1 𝑦 𝑥𝐴 𝐵
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2111  {cab 2776  Ⅎwnfc 2936  ∀wral 3106  ∩ ciin 4883 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-iin 4885 This theorem is referenced by:  iinab  4954  fnlimcnv  42352  fnlimfvre  42359  fnlimabslt  42364  iinhoiicc  43356  preimageiingt  43398  preimaleiinlt  43399  smflimlem6  43452  smflim  43453  smflim2  43480  smfsup  43488  smfsupmpt  43489  smfsupxr  43490  smfinflem  43491  smfinf  43492  smfinfmpt  43493  smflimsup  43502  smfliminf  43505
 Copyright terms: Public domain W3C validator