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

Theorem cbvrex 3026
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 2610 . 2  |-  F/_ x A
2 nfcv 2610 . 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 3024 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 1590   E.wrex 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1588  df-nf 1591  df-sb 1702  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ral 2797  df-rex 2798
This theorem is referenced by:  cbvrmo  3028  cbvrexv  3030  cbvrexsv  3041  cbviun  4291  isarep1  5581  elabrex  6045  onminex  6504  boxcutc  7392  indexfi  7706  wdom2d  7882  hsmexlem2  8683  iundisj  21131  mbfsup  21244  iundisjf  26051  iundisjfi  26200  voliune  26765  volfiniune  26766  cvmcov  27272  indexa  28751  rexrabdioph  29256  rexfrabdioph  29257  stoweidlem31  29950  stoweidlem59  29978  rexsb  30116  cbvrex2  30121  bnj1542  32132
  Copyright terms: Public domain W3C validator