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

Theorem cbvral2v 3076
Description: Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by NM, 10-Aug-2004.)
Hypotheses
Ref Expression
cbvral2v.1  |-  ( x  =  z  ->  ( ph 
<->  ch ) )
cbvral2v.2  |-  ( y  =  w  ->  ( ch 
<->  ps ) )
Assertion
Ref Expression
cbvral2v  |-  ( A. x  e.  A  A. y  e.  B  ph  <->  A. z  e.  A  A. w  e.  B  ps )
Distinct variable groups:    x, A    z, A    x, y, B   
y, z, B    w, B    ph, z    ps, y    ch, x    ch, w
Allowed substitution hints:    ph( x, y, w)    ps( x, z, w)    ch( y, z)    A( y, w)

Proof of Theorem cbvral2v
StepHypRef Expression
1 cbvral2v.1 . . . 4  |-  ( x  =  z  ->  ( ph 
<->  ch ) )
21ralbidv 2880 . . 3  |-  ( x  =  z  ->  ( A. y  e.  B  ph  <->  A. y  e.  B  ch ) )
32cbvralv 3068 . 2  |-  ( A. x  e.  A  A. y  e.  B  ph  <->  A. z  e.  A  A. y  e.  B  ch )
4 cbvral2v.2 . . . 4  |-  ( y  =  w  ->  ( ch 
<->  ps ) )
54cbvralv 3068 . . 3  |-  ( A. y  e.  B  ch  <->  A. w  e.  B  ps )
65ralbii 2872 . 2  |-  ( A. z  e.  A  A. y  e.  B  ch  <->  A. z  e.  A  A. w  e.  B  ps )
73, 6bitri 249 1  |-  ( A. x  e.  A  A. y  e.  B  ph  <->  A. z  e.  A  A. w  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wral 2791
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
This theorem is referenced by:  cbvral3v  3078  fununi  5640  fiint  7795  nqereu  9305  mhmpropd  15841  efgred  16635  mplcoe5  17999  mdetunilem9  18989  fbun  20207  fbunfip  20236  caucfil  21588  pmltpc  21728  axcontlem10  24141  frgrawopreglem5  24913  ghgrplem2OLD  25234  htth  25700  cdj3lem3b  27224  cdj3i  27225  nofulllem5  29434  mgmhmpropd  32307  fipjust  37415
  Copyright terms: Public domain W3C validator