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 3214
Description: Version of r19.41v 3178 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 3178 . . 3 (∃𝑦𝐵 (𝜑𝜓) ↔ (∃𝑦𝐵 𝜑𝜓))
21rexbii 3083 . 2 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ ∃𝑥𝐴 (∃𝑦𝐵 𝜑𝜓))
3 r19.41v 3178 . 2 (∃𝑥𝐴 (∃𝑦𝐵 𝜑𝜓) ↔ (∃𝑥𝐴𝑦𝐵 𝜑𝜓))
42, 3bitri 274 1 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∃𝑥𝐴𝑦𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  wrex 3059
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 3060
This theorem is referenced by:  genpass  11034  mulsuniflem  28099  addsdilem2  28102  mulsasslem1  28113  mulsasslem2  28114  dfcgra2  28706  axeuclid  28846  wspthsnwspthsnon  29799  dya2iocnrect  34032  satfv0  35099  satfv1  35104  satf0  35113  itg2addnclem3  37277  prprelprb  46994  prprspr2  46995
  Copyright terms: Public domain W3C validator