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

Theorem cbvrex2v 2941
Description: Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by FL, 2-Jul-2012.)
Hypotheses
Ref Expression
cbvrex2v.1  |-  ( x  =  z  ->  ( ph 
<->  ch ) )
cbvrex2v.2  |-  ( y  =  w  ->  ( ch 
<->  ps ) )
Assertion
Ref Expression
cbvrex2v  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. z  e.  A  E. w  e.  B  ps )
Distinct variable groups:    x, A    z, A    w, B    x, B, y    z, B, y    ch, w    ch, x    ph, z    ps, y
Allowed substitution hints:    ph( x, y, w)    ps( x, z, w)    ch( y, z)    A( y, w)

Proof of Theorem cbvrex2v
StepHypRef Expression
1 cbvrex2v.1 . . . 4  |-  ( x  =  z  ->  ( ph 
<->  ch ) )
21rexbidv 2726 . . 3  |-  ( x  =  z  ->  ( E. y  e.  B  ph  <->  E. y  e.  B  ch ) )
32cbvrexv 2933 . 2  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. z  e.  A  E. y  e.  B  ch )
4 cbvrex2v.2 . . . 4  |-  ( y  =  w  ->  ( ch 
<->  ps ) )
54cbvrexv 2933 . . 3  |-  ( E. y  e.  B  ch  <->  E. w  e.  B  ps )
65rexbii 2730 . 2  |-  ( E. z  e.  A  E. y  e.  B  ch  <->  E. z  e.  A  E. w  e.  B  ps )
73, 6bitri 241 1  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. z  e.  A  E. w  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wrex 2706
This theorem is referenced by:  omeu  6828  oeeui  6845  eroveu  6999  genpv  8876  bezoutlem3  13040  bezoutlem4  13041  bezout  13042  4sqlem2  13317  vdwnn  13366  efgrelexlema  15381  dyadmax  19490  2sqlem9  21157  2sq  21160  pstmfval  24291  nn0prpwlem  26325  isbnd2  26492
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710  df-rex 2711
  Copyright terms: Public domain W3C validator