Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbviunv Unicode version

Theorem cbviunv 4369
 Description: Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 15-Sep-2003.)
Hypothesis
Ref Expression
cbviunv.1
Assertion
Ref Expression
cbviunv
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem cbviunv
StepHypRef Expression
1 nfcv 2619 . 2
2 nfcv 2619 . 2
3 cbviunv.1 . 2
41, 2, 3cbviun 4367 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  =wceq 1395  U_ciun 4330 This theorem is referenced by:  iunxdif2  4378  otiunsndisj  4758  onfununi  7031  oelim2  7263  marypha2lem2  7916  trcl  8180  r1om  8645  fictb  8646  cfsmolem  8671  cfsmo  8672  domtriomlem  8843  domtriom  8844  pwfseq  9063  wunex2  9137  wuncval2  9146  fsuppmapnn0fiubex  12098  ackbijnn  13640  efgs1b  16754  ablfaclem3  17138  ptbasfi  20082  bcth3  21770  itg1climres  22121  2spotiundisj  25062  hashunif  27605  cvmliftlem15  28743  trpredlem1  29310  trpredtr  29313  trpredmintr  29314  trpredrec  29321  neibastop2  30179  filnetlem4  30199  sstotbnd2  30270  heiborlem3  30309  heibor  30317  otiunsndisjX  32301  bnj601  33978  lcfr  37312  mapdrval  37374 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-iun 4332
 Copyright terms: Public domain W3C validator