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

Step	Hyp	Ref	Expression
1		nfcv 2619	. 2
2		nfcv 2619	. 2
3		cbviunv.1	. 2
4	1, 2, 3	cbviun 4367	1

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