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

Theorem nfiin 4748
Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.)
Hypotheses
Ref Expression
nfiun.1 𝑦𝐴
nfiun.2 𝑦𝐵
Assertion
Ref Expression
nfiin 𝑦 𝑥𝐴 𝐵

Proof of Theorem nfiin
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-iin 4722 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∀𝑥𝐴 𝑧𝐵}
2 nfiun.1 . . . 4 𝑦𝐴
3 nfiun.2 . . . . 5 𝑦𝐵
43nfcri 2949 . . . 4 𝑦 𝑧𝐵
52, 4nfral 3140 . . 3 𝑦𝑥𝐴 𝑧𝐵
65nfab 2960 . 2 𝑦{𝑧 ∣ ∀𝑥𝐴 𝑧𝐵}
71, 6nfcxfr 2953 1 𝑦 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2157  {cab 2799  wnfc 2942  wral 3103   ciin 4720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-iin 4722
This theorem is referenced by:  iinab  4780  fnlimcnv  40380  fnlimfvre  40387  fnlimabslt  40392  iinhoiicc  41371  preimageiingt  41413  preimaleiinlt  41414  smflimlem6  41467  smflim  41468  smflim2  41495  smfsup  41503  smfsupmpt  41504  smfsupxr  41505  smfinflem  41506  smfinf  41507  smfinfmpt  41508  smflimsup  41517  smfliminf  41520
  Copyright terms: Public domain W3C validator