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

Theorem r19.41vv 3222
Description: Version of r19.41v 3186 with two quantifiers. (Contributed by Thierry Arnoux, 25-Jan-2017.)
Assertion
Ref Expression
r19.41vv (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∃𝑥𝐴𝑦𝐵 𝜑𝜓))
Distinct variable groups:   𝜓,𝑥   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem r19.41vv
StepHypRef Expression
1 r19.41v 3186 . . 3 (∃𝑦𝐵 (𝜑𝜓) ↔ (∃𝑦𝐵 𝜑𝜓))
21rexbii 3091 . 2 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ ∃𝑥𝐴 (∃𝑦𝐵 𝜑𝜓))
3 r19.41v 3186 . 2 (∃𝑥𝐴 (∃𝑦𝐵 𝜑𝜓) ↔ (∃𝑥𝐴𝑦𝐵 𝜑𝜓))
42, 3bitri 274 1 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∃𝑥𝐴𝑦𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  wrex 3067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3068
This theorem is referenced by:  genpass  11040  mulsuniflem  28069  addsdilem2  28072  mulsasslem1  28083  mulsasslem2  28084  dfcgra2  28654  axeuclid  28794  wspthsnwspthsnon  29747  dya2iocnrect  33934  satfv0  35001  satfv1  35006  satf0  35015  itg2addnclem3  37179  prprelprb  46886  prprspr2  46887
  Copyright terms: Public domain W3C validator