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

Theorem cbvral2v 3061
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 2846 . . 3  |-  ( x  =  z  ->  ( A. y  e.  B  ph  <->  A. y  e.  B  ch ) )
32cbvralv 3053 . 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 3053 . . 3  |-  ( A. y  e.  B  ch  <->  A. w  e.  B  ps )
65ralbii 2839 . 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 2799
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-ex 1588  df-nf 1591  df-sb 1703  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804
This theorem is referenced by:  cbvral3v  3063  fununi  5593  fiint  7700  nqereu  9210  mhmpropd  15590  efgred  16367  mplcoe5  17673  mdetunilem9  18559  fbun  19546  fbunfip  19575  caucfil  20927  pmltpc  21067  axcontlem10  23372  ghgrplem2  24007  htth  24473  cdj3lem3b  25997  cdj3i  25998  nofulllem5  27992  frgrawopreglem5  30790  dmatsubcl  31057
  Copyright terms: Public domain W3C validator