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

Theorem nfiun 4940
Description: Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2381. See nfiung 4942 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 4912 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
2 nfiun.1 . . . 4 𝑦𝐴
3 nfiun.2 . . . . 5 𝑦𝐵
43nfcri 2968 . . . 4 𝑦 𝑧𝐵
52, 4nfrex 3306 . . 3 𝑦𝑥𝐴 𝑧𝐵
65nfab 2981 . 2 𝑦{𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
71, 6nfcxfr 2972 1 𝑦 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  {cab 2796  wnfc 2958  wrex 3136   ciun 4910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-iun 4912
This theorem is referenced by:  iunab  4966  disjxiun  5054  ovoliunnul  24035  iundisjf  30267  iundisj2f  30268  iundisjfi  30445  iundisj2fi  30446  bnj1498  32230  trpredlem1  32963  trpredrec  32974  ss2iundf  39882  nfcoll  40469  fnlimcnv  41824  fnlimfvre  41831  fnlimabslt  41836  smfaddlem1  42916  smflimlem6  42929  smflim  42930  smfmullem4  42946  smflim2  42957  smflimsup  42979  smfliminf  42982
  Copyright terms: Public domain W3C validator