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

Theorem cbvral2v 3171
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 2982 . . 3 (𝑥 = 𝑧 → (∀𝑦𝐵 𝜑 ↔ ∀𝑦𝐵 𝜒))
32cbvralv 3163 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑧𝐴𝑦𝐵 𝜒)
4 cbvral2v.2 . . . 4 (𝑦 = 𝑤 → (𝜒𝜓))
54cbvralv 3163 . . 3 (∀𝑦𝐵 𝜒 ↔ ∀𝑤𝐵 𝜓)
65ralbii 2976 . 2 (∀𝑧𝐴𝑦𝐵 𝜒 ↔ ∀𝑧𝐴𝑤𝐵 𝜓)
73, 6bitri 264 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑧𝐴𝑤𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wral 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913
This theorem is referenced by:  cbvral3v  3173  fununi  5932  fiint  8197  nqereu  9711  mhmpropd  17281  efgred  18101  mplcoe5  19408  mdetunilem9  20366  fbun  21584  fbunfip  21613  caucfil  23021  pmltpc  23159  iscgrglt  25343  axcontlem10  25787  frgrwopreglem5  27077  htth  27663  cdj3lem3b  29187  cdj3i  29188  isros  30054  rossros  30066  fipjust  37390  isotone1  37867  isotone2  37868  ntrclsiso  37886  ntrclskb  37888  ntrclsk3  37889  ntrclsk13  37890  pimincfltioo  40265  incsmf  40288  decsmf  40312  mgmhmpropd  41103
  Copyright terms: Public domain W3C validator