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

Theorem cbvrex 3052
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 2584 . 2  |-  F/_ x A
2 nfcv 2584 . 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 3050 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   F/wnf 1663   E.wrex 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-ex 1660  df-nf 1664  df-sb 1787  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-rex 2781
This theorem is referenced by:  cbvrmo  3054  cbvrexv  3056  cbvrexsv  3067  cbviun  4333  isarep1  5676  elabrex  6159  onminex  6644  boxcutc  7569  indexfi  7884  wdom2d  8097  hsmexlem2  8857  fprodle  14037  iundisj  22487  mbfsup  22606  iundisjf  28188  iundisjfi  28365  voliune  29047  volfiniune  29048  bnj1542  29663  cvmcov  29981  poimirlem24  31877  poimirlem26  31879  indexa  31973  rexrabdioph  35555  rexfrabdioph  35556  elabrexg  37230  dffo3f  37299  disjrnmpt2  37312  stoweidlem31  37711  stoweidlem59  37739  rexsb  38301  cbvrex2  38306
  Copyright terms: Public domain W3C validator