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

Theorem cbvral2v 2932
 Description: Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by NM, 10-Aug-2004.)
Hypotheses
Ref Expression
cbvral2v.1
cbvral2v.2
Assertion
Ref Expression
cbvral2v
Distinct variable groups:   ,   ,   ,,   ,,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,,)   (,,)   (,)   (,)

Proof of Theorem cbvral2v
StepHypRef Expression
1 cbvral2v.1 . . . 4
21ralbidv 2717 . . 3
32cbvralv 2924 . 2
4 cbvral2v.2 . . . 4
54cbvralv 2924 . . 3
65ralbii 2721 . 2
73, 6bitri 241 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177  wral 2697 This theorem is referenced by:  cbvral3v  2934  fununi  5509  fiint  7375  nqereu  8798  mhmpropd  14736  efgred  15372  fbun  17864  fbunfip  17893  caucfil  19228  pmltpc  19339  ghgrplem2  21947  htth  22413  cdj3lem3b  23935  cdj3i  23936  nofulllem5  25653  axcontlem10  25904  frgrawopreglem5  28374 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702
 Copyright terms: Public domain W3C validator