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

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
StepHypRef Expression
1 nfcv 2616 . 2
2 nfcv 2616 . 2
3 cbvral.1 . 2
4 cbvral.2 . 2
5 cbvral.3 . 2
61, 2, 3, 4, 5cbvrexf 3051 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator