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

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