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

Theorem nfiun 5027
Description: Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2365. See nfiung 5029 for a less restrictive version requiring more axioms. (Revised by GG, 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 4999 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
2 nfiun.1 . . . 4 𝑦𝐴
3 nfiun.2 . . . . 5 𝑦𝐵
43nfcri 2882 . . . 4 𝑦 𝑧𝐵
52, 4nfrexw 3300 . . 3 𝑦𝑥𝐴 𝑧𝐵
65nfab 2897 . 2 𝑦{𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
71, 6nfcxfr 2889 1 𝑦 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2098  {cab 2702  wnfc 2875  wrex 3059   ciun 4997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-iun 4999
This theorem is referenced by:  iunab  5055  disjxiun  5146  ttrclselem1  9750  ttrclselem2  9751  ovoliunnul  25480  iundisjf  32458  iundisj2f  32459  iundisjfi  32646  iundisj2fi  32647  bnj1498  34820  ss2iundf  43228  nfcoll  43832  fnlimcnv  45190  fnlimfvre  45197  fnlimabslt  45202  smfaddlem1  46286  smflimlem6  46299  smflim  46300  smfmullem4  46317  smflim2  46329  smflimsup  46351  smfliminf  46354  fsupdm  46365  finfdm  46369
  Copyright terms: Public domain W3C validator