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

Theorem cbvrex2v 3062
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 2868 . . 3  |-  ( x  =  z  ->  ( E. y  e.  B  ph  <->  E. y  e.  B  ch ) )
32cbvrexv 3054 . 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 3054 . . 3  |-  ( E. y  e.  B  ch  <->  E. w  e.  B  ps )
65rexbii 2862 . 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 2800
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 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-rex 2805
This theorem is referenced by:  omeu  7137  oeeui  7154  eroveu  7308  genpv  9283  bezoutlem3  13846  bezoutlem4  13847  bezout  13848  4sqlem2  14132  vdwnn  14181  efgrelexlema  16371  dyadmax  21221  2sqlem9  22855  2sq  22858  legov  23164  pstmfval  26491  nn0prpwlem  28688  isbnd2  28853
  Copyright terms: Public domain W3C validator