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

Theorem cbvrex2vw 3240
Description: Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 3366 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by FL, 2-Jul-2012.) Avoid ax-13 2372. (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 3179 . . 3 (𝑥 = 𝑧 → (∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 𝜒))
32cbvrexvw 3236 . 2 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑧𝐴𝑦𝐵 𝜒)
4 cbvrex2vw.2 . . . 4 (𝑦 = 𝑤 → (𝜒𝜓))
54cbvrexvw 3236 . . 3 (∃𝑦𝐵 𝜒 ↔ ∃𝑤𝐵 𝜓)
65rexbii 3095 . 2 (∃𝑧𝐴𝑦𝐵 𝜒 ↔ ∃𝑧𝐴𝑤𝐵 𝜓)
73, 6bitri 275 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑧𝐴𝑤𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wrex 3071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clel 2811  df-rex 3072
This theorem is referenced by:  omeu  8585  oeeui  8602  eroveu  8806  genpv  10994  bezoutlem3  16483  bezoutlem4  16484  bezout  16485  4sqlem2  16882  vdwnn  16931  efgrelexlema  19617  dyadmax  25115  2sqlem9  26930  2sq  26933  mulsval2lem  27566  precsexlemcbv  27652  legov  27836  dfcgra2  28081  pstmfval  32876  satfv0  34349  satfv0fun  34362  fmla1  34378  nn0prpwlem  35207  isbnd2  36651  nna4b4nsq  41402  oaun3lem1  42124  limsupref  44401  fourierdlem42  44865  fourierdlem54  44876  mogoldbb  46453
  Copyright terms: Public domain W3C validator