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

Theorem nfiun 4954
Description: Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2372. See nfiung 4956 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
nfiun 𝑦 𝑥𝐴 𝐵
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem nfiun
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-iun 4926 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
2 nfiun.1 . . . 4 𝑦𝐴
3 nfiun.2 . . . . 5 𝑦𝐵
43nfcri 2894 . . . 4 𝑦 𝑧𝐵
52, 4nfrex 3242 . . 3 𝑦𝑥𝐴 𝑧𝐵
65nfab 2913 . 2 𝑦{𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
71, 6nfcxfr 2905 1 𝑦 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  {cab 2715  wnfc 2887  wrex 3065   ciun 4924
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-iun 4926
This theorem is referenced by:  iunab  4981  disjxiun  5071  ttrclselem1  9483  ttrclselem2  9484  ovoliunnul  24671  iundisjf  30928  iundisj2f  30929  iundisjfi  31117  iundisj2fi  31118  bnj1498  33041  ss2iundf  41267  nfcoll  41874  fnlimcnv  43208  fnlimfvre  43215  fnlimabslt  43220  smfaddlem1  44298  smflimlem6  44311  smflim  44312  smfmullem4  44328  smflim2  44339  smflimsup  44361  smfliminf  44364
  Copyright terms: Public domain W3C validator