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

Theorem cbvrex 2930
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 2573 . 2  |-  F/_ x A
2 nfcv 2573 . 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 2928 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   F/wnf 1554   E.wrex 2707
This theorem is referenced by:  cbvrmo  2932  cbvrexv  2934  cbvrexsv  2945  cbviun  4129  onminex  4788  isarep1  5533  elabrex  5986  boxcutc  7106  indexfi  7415  wdom2d  7549  hsmexlem2  8308  iundisj  19443  mbfsup  19557  iundisjf  24030  iundisjfi  24153  voliune  24586  volfiniune  24587  cvmcov  24951  indexa  26436  rexrabdioph  26855  rexfrabdioph  26856  stoweidlem31  27757  stoweidlem59  27785  rexsb  27923  cbvrex2  27928  bnj1542  29229
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2711  df-rex 2712
  Copyright terms: Public domain W3C validator