Theorem cbvrex 3053

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)

Hypotheses

Ref	Expression
cbvral.1
cbvral.2
cbvral.3

Assertion

Ref	Expression
cbvrex

Distinct variable groups:   ,   ,

Proof of Theorem cbvrex

Step	Hyp	Ref	Expression
1		nfcv 2616	. 2
2		nfcv 2616	. 2
3		cbvral.1	. 2
4		cbvral.2	. 2
5		cbvral.3	. 2
6	1, 2, 3, 4, 5	cbvrexf 3051	1

Syntax hints:  ->wi 4  <->wb 184  F/wnf 1590  E.wrex 2801

This theorem is referenced by:  cbvrmo  3055  cbvrexv  3057  cbvrexsv  3068  cbviun  4324  isarep1  5616  elabrex  6085  onminex  6551  boxcutc  7440  indexfi  7754  wdom2d  7932  hsmexlem2  8733  iundisj  21429  mbfsup  21542  iundisjf  26399  iundisjfi  26541  voliune  27101  volfiniune  27102  cvmcov  27608  indexa  29087  rexrabdioph  29592  rexfrabdioph  29593  elabrexg  30241  limcperiod  30399  stoweidlem31  30560  stoweidlem59  30588  fourierdlem81  30717  fourierdlem92  30728  rexsb  30869  cbvrex2  30874  bnj1542  32693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1588  df-nf 1591  df-sb 1703  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2805  df-rex 2806