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

Theorem cbvrex2vw 3227
Description: Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 3341 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by FL, 2-Jul-2012.) Avoid ax-13 2371. (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 3172 . . 3 (𝑥 = 𝑧 → (∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 𝜒))
32cbvrexvw 3225 . 2 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑧𝐴𝑦𝐵 𝜒)
4 cbvrex2vw.2 . . . 4 (𝑦 = 𝑤 → (𝜒𝜓))
54cbvrexvw 3225 . . 3 (∃𝑦𝐵 𝜒 ↔ ∃𝑤𝐵 𝜓)
65rexbii 3094 . 2 (∃𝑧𝐴𝑦𝐵 𝜒 ↔ ∃𝑧𝐴𝑤𝐵 𝜓)
73, 6bitri 275 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑧𝐴𝑤𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wrex 3070
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 3071
This theorem is referenced by:  omeu  8533  oeeui  8550  eroveu  8754  genpv  10940  bezoutlem3  16427  bezoutlem4  16428  bezout  16429  4sqlem2  16826  vdwnn  16875  efgrelexlema  19536  dyadmax  24978  2sqlem9  26791  2sq  26794  legov  27569  dfcgra2  27814  pstmfval  32534  satfv0  34009  satfv0fun  34022  fmla1  34038  nn0prpwlem  34840  isbnd2  36288  nna4b4nsq  41041  oaun3lem1  41733  limsupref  44012  fourierdlem42  44476  fourierdlem54  44487  mogoldbb  46063
  Copyright terms: Public domain W3C validator