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

Theorem nfiun 4946
Description: Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2385. See nfiung 4948 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 4919 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
2 nfiun.1 . . . 4 𝑦𝐴
3 nfiun.2 . . . . 5 𝑦𝐵
43nfcri 2976 . . . 4 𝑦 𝑧𝐵
52, 4nfrex 3314 . . 3 𝑦𝑥𝐴 𝑧𝐵
65nfab 2989 . 2 𝑦{𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
71, 6nfcxfr 2980 1 𝑦 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  {cab 2804  wnfc 2966  wrex 3144   ciun 4917
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-iun 4919
This theorem is referenced by:  iunab  4972  disjxiun  5060  ovoliunnul  24042  iundisjf  30273  iundisj2f  30274  iundisjfi  30451  iundisj2fi  30452  bnj1498  32236  trpredlem1  32969  trpredrec  32980  ss2iundf  39888  nfcoll  40476  fnlimcnv  41832  fnlimfvre  41839  fnlimabslt  41844  smfaddlem1  42924  smflimlem6  42937  smflim  42938  smfmullem4  42954  smflim2  42965  smflimsup  42987  smfliminf  42990
  Copyright terms: Public domain W3C validator