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

Theorem nfiu1 4753
Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.)
Assertion
Ref Expression
nfiu1 𝑥 𝑥𝐴 𝐵

Proof of Theorem nfiu1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-iun 4725 . 2 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
2 nfre1 3203 . . 3 𝑥𝑥𝐴 𝑦𝐵
32nfab 2964 . 2 𝑥{𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
41, 3nfcxfr 2957 1 𝑥 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2157  {cab 2803  wnfc 2946  wrex 3108   ciun 4723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rex 3113  df-iun 4725
This theorem is referenced by:  ssiun2s  4767  disjxiun  4852  triun  4970  iunopeqop  5189  eliunxp  5475  opeliunxp2  5476  opeliunxp2f  7581  ixpf  8177  ixpiunwdom  8745  r1val1  8906  rankuni2b  8973  rankval4  8987  cplem2  9010  ac6num  9596  iunfo  9656  iundom2g  9657  inar1  9892  tskuni  9900  gsum2d2lem  18593  gsum2d2  18594  gsumcom2  18595  iunconn  21466  ptclsg  21653  cnextfvval  22103  ssiun2sf  29726  aciunf1lem  29812  fsumiunle  29925  esum2dlem  30502  esum2d  30503  esumiun  30504  sigapildsys  30573  bnj958  31355  bnj1000  31356  bnj981  31365  bnj1398  31447  bnj1408  31449  iunconnlem2  39683  iunmapss  39912  iunmapsn  39914  allbutfi  40113  fsumiunss  40305  dvnprodlem1  40659  dvnprodlem2  40660  sge0iunmptlemfi  41127  sge0iunmptlemre  41129  sge0iunmpt  41132  iundjiun  41174  voliunsge0lem  41186  caratheodorylem2  41241  smflimmpt  41516  smflimsuplem7  41532  eliunxp2  42698
  Copyright terms: Public domain W3C validator