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

Theorem cbvrex2vw 3374
 Description: Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 3377 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by FL, 2-Jul-2012.) (Revised by Gino Giotto, 10-Jan-2024.)
Hypotheses
Ref Expression
cbvrex2vw.1 (𝑥 = 𝑧 → (𝜑𝜒))
cbvrex2vw.2 (𝑦 = 𝑤 → (𝜒𝜓))
Assertion
Ref Expression
cbvrex2vw (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑧𝐴𝑤𝐵 𝜓)
Distinct variable groups:   𝑥,𝑧   𝑦,𝑤   𝑥,𝐴,𝑧   𝑤,𝐵   𝑥,𝐵,𝑦,𝑧   𝜒,𝑤   𝜒,𝑥   𝜑,𝑧   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑤)   𝜓(𝑥,𝑧,𝑤)   𝜒(𝑦,𝑧)   𝐴(𝑦,𝑤)

Proof of Theorem cbvrex2vw
StepHypRef Expression
1 cbvrex2vw.1 . . . 4 (𝑥 = 𝑧 → (𝜑𝜒))
21rexbidv 3221 . . 3 (𝑥 = 𝑧 → (∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 𝜒))
32cbvrexvw 3362 . 2 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑧𝐴𝑦𝐵 𝜒)
4 cbvrex2vw.2 . . . 4 (𝑦 = 𝑤 → (𝜒𝜓))
54cbvrexvw 3362 . . 3 (∃𝑦𝐵 𝜒 ↔ ∃𝑤𝐵 𝜓)
65rexbii 3175 . 2 (∃𝑧𝐴𝑦𝐵 𝜒 ↔ ∃𝑧𝐴𝑤𝐵 𝜓)
73, 6bitri 278 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑧𝐴𝑤𝐵 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∃wrex 3071 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-clel 2830  df-rex 3076 This theorem is referenced by:  omeu  8221  oeeui  8238  eroveu  8402  genpv  10459  bezoutlem3  15940  bezoutlem4  15941  bezout  15942  4sqlem2  16340  vdwnn  16389  efgrelexlema  18942  dyadmax  24298  2sqlem9  26110  2sq  26113  legov  26478  dfcgra2  26723  pstmfval  31367  satfv0  32836  satfv0fun  32849  fmla1  32865  nn0prpwlem  34060  isbnd2  35501  nna4b4nsq  39989  limsupref  42693  fourierdlem42  43157  fourierdlem54  43168  mogoldbb  44670
 Copyright terms: Public domain W3C validator