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

Theorem nfiin 5050
Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2374. See nfiing 5052 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 5022 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∀𝑥𝐴 𝑧𝐵}
2 nfiun.1 . . . 4 𝑦𝐴
3 nfiun.2 . . . . 5 𝑦𝐵
43nfcri 2895 . . . 4 𝑦 𝑧𝐵
52, 4nfralw 3312 . . 3 𝑦𝑥𝐴 𝑧𝐵
65nfab 2910 . 2 𝑦{𝑧 ∣ ∀𝑥𝐴 𝑧𝐵}
71, 6nfcxfr 2902 1 𝑦 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2103  {cab 2711  wnfc 2888  wral 3063   ciin 5020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ral 3064  df-iin 5022
This theorem is referenced by:  iinab  5094  fnlimcnv  45522  fnlimfvre  45529  fnlimabslt  45534  iinhoiicc  46529  preimageiingt  46575  preimaleiinlt  46576  smflimlem6  46631  smflim  46632  smflim2  46661  smfsup  46669  smfsupmpt  46670  smfsupxr  46671  smfinflem  46672  smfinf  46673  smfinfmpt  46674  smflimsup  46683  smfliminf  46686  fsupdm  46697  finfdm  46701
  Copyright terms: Public domain W3C validator