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

Theorem cbvrex 2774
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 2432 . 2  |-  F/_ x A
2 nfcv 2432 . 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 2772 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   F/wnf 1534   E.wrex 2557
This theorem is referenced by:  cbvrmo  2776  cbvrexv  2778  cbvrexsv  2789  cbviun  3955  onminex  4614  isarep1  5347  elabrex  5781  boxcutc  6875  indexfi  7179  wdom2d  7310  hsmexlem2  8069  iundisj  18921  mbfsup  19035  iundisjfi  23378  iundisjf  23380  cvmcov  23809  indexa  26515  rexrabdioph  26978  rexfrabdioph  26979  stoweidlem31  27883  stoweidlem59  27911  rexsb  28049  cbvrex2  28054  bnj1542  29205
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator