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

Theorem cbvral2v 3362
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 3167 . . 3 (𝑥 = 𝑧 → (∀𝑦𝐵 𝜑 ↔ ∀𝑦𝐵 𝜒))
32cbvralv 3354 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑧𝐴𝑦𝐵 𝜒)
4 cbvral2v.2 . . . 4 (𝑦 = 𝑤 → (𝜒𝜓))
54cbvralv 3354 . . 3 (∀𝑦𝐵 𝜒 ↔ ∀𝑤𝐵 𝜓)
65ralbii 3161 . 2 (∀𝑧𝐴𝑦𝐵 𝜒 ↔ ∀𝑧𝐴𝑤𝐵 𝜓)
73, 6bitri 267 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑧𝐴𝑤𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wral 3089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clel 2795  df-nfc 2930  df-ral 3094
This theorem is referenced by:  cbvral3v  3364  fununi  6175  fiint  8479  nqereu  10039  mhmpropd  17656  efgred  18476  mplcoe5  19791  mdetunilem9  20752  fbun  21972  fbunfip  22001  caucfil  23409  pmltpc  23558  iscgrglt  25765  axcontlem10  26210  htth  28300  cdj3lem3b  29824  cdj3i  29825  isros  30747  rossros  30759  fipjust  38653  isotone1  39128  isotone2  39129  ntrclsiso  39147  ntrclskb  39149  ntrclsk3  39150  ntrclsk13  39151  pimincfltioo  41674  incsmf  41697  decsmf  41721  mgmhmpropd  42584
  Copyright terms: Public domain W3C validator