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

Theorem cbvral2v 3089
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 2893 . . 3  |-  ( x  =  z  ->  ( A. y  e.  B  ph  <->  A. y  e.  B  ch ) )
32cbvralv 3081 . 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 3081 . . 3  |-  ( A. y  e.  B  ch  <->  A. w  e.  B  ps )
65ralbii 2885 . 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 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1618  df-nf 1622  df-sb 1745  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809
This theorem is referenced by:  cbvral3v  3091  fununi  5636  fiint  7789  nqereu  9296  mhmpropd  16171  efgred  16965  mplcoe5  18326  mdetunilem9  19289  fbun  20507  fbunfip  20536  caucfil  21888  pmltpc  22028  axcontlem10  24478  frgrawopreglem5  25250  ghgrplem2OLD  25567  htth  26033  cdj3lem3b  27557  cdj3i  27558  nofulllem5  29706  mgmhmpropd  32845  fipjust  38163
  Copyright terms: Public domain W3C validator