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

Theorem nfiun 5049
Description: Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2374. See nfiung 5051 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 5021 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
2 nfiun.1 . . . 4 𝑦𝐴
3 nfiun.2 . . . . 5 𝑦𝐵
43nfcri 2895 . . . 4 𝑦 𝑧𝐵
52, 4nfrexw 3314 . . 3 𝑦𝑥𝐴 𝑧𝐵
65nfab 2910 . 2 𝑦{𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
71, 6nfcxfr 2902 1 𝑦 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2103  {cab 2711  wnfc 2888  wrex 3072   ciun 5019
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ral 3064  df-rex 3073  df-iun 5021
This theorem is referenced by:  iunab  5077  disjxiun  5166  ttrclselem1  9790  ttrclselem2  9791  ovoliunnul  25554  iundisjf  32602  iundisj2f  32603  iundisjfi  32793  iundisj2fi  32794  bnj1498  35029  ss2iundf  43561  nfcoll  44165  fnlimcnv  45522  fnlimfvre  45529  fnlimabslt  45534  smfaddlem1  46618  smflimlem6  46631  smflim  46632  smfmullem4  46649  smflim2  46661  smflimsup  46683  smfliminf  46686  fsupdm  46697  finfdm  46701
  Copyright terms: Public domain W3C validator