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

Theorem cbvrex 3085
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  |-  F/ y
ph
cbvral.2  |-  F/ x ps
cbvral.3  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvrex  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Distinct variable groups:    x, A    y, A
Allowed substitution hints:    ph( x, y)    ps( x, y)

Proof of Theorem cbvrex
StepHypRef Expression
1 nfcv 2629 . 2  |-  F/_ x A
2 nfcv 2629 . 2  |-  F/_ y A
3 cbvral.1 . 2  |-  F/ y
ph
4 cbvral.2 . 2  |-  F/ x ps
5 cbvral.3 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
61, 2, 3, 4, 5cbvrexf 3083 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   F/wnf 1599   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1597  df-nf 1600  df-sb 1712  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820
This theorem is referenced by:  cbvrmo  3087  cbvrexv  3089  cbvrexsv  3100  cbviun  4362  isarep1  5665  elabrex  6141  onminex  6620  boxcutc  7509  indexfi  7824  wdom2d  8002  hsmexlem2  8803  iundisj  21693  mbfsup  21806  iundisjf  27121  iundisjfi  27269  voliune  27841  volfiniune  27842  cvmcov  28348  indexa  29827  rexrabdioph  30331  rexfrabdioph  30332  elabrexg  31012  limcperiod  31170  stoweidlem31  31331  stoweidlem59  31359  fourierdlem81  31488  fourierdlem92  31499  rexsb  31640  cbvrex2  31645  bnj1542  32994
  Copyright terms: Public domain W3C validator