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  8581  oeeui  8598  eroveu  8802  genpv  10990  bezoutlem3  16479  bezoutlem4  16480  bezout  16481  4sqlem2  16878  vdwnn  16927  efgrelexlema  19610  dyadmax  25097  2sqlem9  26910  2sq  26913  mulsval2lem  27546  precsexlemcbv  27632  legov  27816  dfcgra2  28061  pstmfval  32814  satfv0  34287  satfv0fun  34300  fmla1  34316  nn0prpwlem  35145  isbnd2  36589  nna4b4nsq  41346  oaun3lem1  42057  limsupref  44336  fourierdlem42  44800  fourierdlem54  44811  mogoldbb  46388
  Copyright terms: Public domain W3C validator