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

Theorem 2ex2rexrot 3213
 Description: Rotate two existential quantifiers and two restricted existential quantifiers. (Contributed by AV, 9-Nov-2023.)
Assertion
Ref Expression
2ex2rexrot (∃𝑥𝑦𝑧𝐴𝑤𝐵 𝜑 ↔ ∃𝑧𝐴𝑤𝐵𝑥𝑦𝜑)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝑥,𝐵   𝑦,𝐵   𝑥,𝑤   𝑦,𝑤   𝑥,𝑧   𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤)   𝐴(𝑧,𝑤)   𝐵(𝑧,𝑤)

Proof of Theorem 2ex2rexrot
StepHypRef Expression
1 rexcom4 3212 . . 3 (∃𝑤𝐵𝑥𝑦𝜑 ↔ ∃𝑥𝑤𝐵𝑦𝜑)
21rexbii 3210 . 2 (∃𝑧𝐴𝑤𝐵𝑥𝑦𝜑 ↔ ∃𝑧𝐴𝑥𝑤𝐵𝑦𝜑)
3 rexcom4 3212 . 2 (∃𝑧𝐴𝑥𝑤𝐵𝑦𝜑 ↔ ∃𝑥𝑧𝐴𝑤𝐵𝑦𝜑)
4 rexcom4 3212 . . . . 5 (∃𝑤𝐵𝑦𝜑 ↔ ∃𝑦𝑤𝐵 𝜑)
54rexbii 3210 . . . 4 (∃𝑧𝐴𝑤𝐵𝑦𝜑 ↔ ∃𝑧𝐴𝑦𝑤𝐵 𝜑)
6 rexcom4 3212 . . . 4 (∃𝑧𝐴𝑦𝑤𝐵 𝜑 ↔ ∃𝑦𝑧𝐴𝑤𝐵 𝜑)
75, 6bitri 278 . . 3 (∃𝑧𝐴𝑤𝐵𝑦𝜑 ↔ ∃𝑦𝑧𝐴𝑤𝐵 𝜑)
87exbii 1849 . 2 (∃𝑥𝑧𝐴𝑤𝐵𝑦𝜑 ↔ ∃𝑥𝑦𝑧𝐴𝑤𝐵 𝜑)
92, 3, 83bitrri 301 1 (∃𝑥𝑦𝑧𝐴𝑤𝐵 𝜑 ↔ ∃𝑧𝐴𝑤𝐵𝑥𝑦𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209  ∃wex 1781  ∃wrex 3107 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-11 2158 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3112 This theorem is referenced by:  satfv1  32738
 Copyright terms: Public domain W3C validator