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

Theorem cbvrex 3018
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 2594 . 2  |-  F/_ x A
2 nfcv 2594 . 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 3016 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   F/wnf 1669   E.wrex 2740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ex 1666  df-nf 1670  df-sb 1800  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ral 2744  df-rex 2745
This theorem is referenced by:  cbvrmo  3020  cbvrexv  3022  cbvrexsv  3033  cbviun  4318  isarep1  5667  elabrex  6153  onminex  6639  boxcutc  7570  indexfi  7887  wdom2d  8100  hsmexlem2  8862  fprodle  14062  iundisj  22513  mbfsup  22632  iundisjf  28211  iundisjfi  28384  voliune  29064  volfiniune  29065  bnj1542  29680  cvmcov  29998  poimirlem24  31976  poimirlem26  31978  indexa  32072  rexrabdioph  35649  rexfrabdioph  35650  elabrexg  37380  dffo3f  37460  disjrnmpt2  37473  stoweidlem31  37902  stoweidlem59  37930  rexsb  38599  cbvrex2  38604
  Copyright terms: Public domain W3C validator