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

Theorem cbvrex2v 3077
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 2952 . . 3  |-  ( x  =  z  ->  ( E. y  e.  B  ph  <->  E. y  e.  B  ch ) )
32cbvrexv 3069 . 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 3069 . . 3  |-  ( E. y  e.  B  ch  <->  E. w  e.  B  ps )
65rexbii 2943 . 2  |-  ( E. z  e.  A  E. y  e.  B  ch  <->  E. z  e.  A  E. w  e.  B  ps )
73, 6bitri 249 1  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. z  e.  A  E. w  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wrex 2792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1598  df-nf 1602  df-sb 1725  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796  df-rex 2797
This theorem is referenced by:  omeu  7232  oeeui  7249  eroveu  7404  genpv  9375  bezoutlem3  14050  bezoutlem4  14051  bezout  14052  4sqlem2  14339  vdwnn  14388  efgrelexlema  16636  dyadmax  21873  2sqlem9  23513  2sq  23516  legov  23837  pstmfval  27741  nn0prpwlem  30108  isbnd2  30247  fourierdlem42  31816  fourierdlem54  31828
  Copyright terms: Public domain W3C validator