Theorem cbvrex 3081

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 2619	. 2
2		nfcv 2619	. 2
3		cbvral.1	. 2
4		cbvral.2	. 2
5		cbvral.3	. 2
6	1, 2, 3, 4, 5	cbvrexf 3079	1

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

This theorem is referenced by:  cbvrmo  3083  cbvrexv  3085  cbvrexsv  3096  cbviun  4367  isarep1  5672  elabrex  6155  onminex  6642  boxcutc  7532  indexfi  7848  wdom2d  8027  hsmexlem2  8828  iundisj  21958  mbfsup  22071  iundisjf  27448  iundisjfi  27601  voliune  28201  volfiniune  28202  cvmcov  28708  indexa  30224  rexrabdioph  30727  rexfrabdioph  30728  elabrexg  31430  fprodle  31604  stoweidlem31  31813  stoweidlem59  31841  rexsb  32173  cbvrex2  32178  bnj1542  33915

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-ex 1613  df-nf 1617  df-sb 1740  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813