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 3218
Description: Version of r19.41v 3182 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 3182 . . 3 (∃𝑦𝐵 (𝜑𝜓) ↔ (∃𝑦𝐵 𝜑𝜓))
21rexbii 3088 . 2 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ ∃𝑥𝐴 (∃𝑦𝐵 𝜑𝜓))
3 r19.41v 3182 . 2 (∃𝑥𝐴 (∃𝑦𝐵 𝜑𝜓) ↔ (∃𝑥𝐴𝑦𝐵 𝜑𝜓))
42, 3bitri 275 1 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∃𝑥𝐴𝑦𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 395  wrex 3064
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 396  df-ex 1774  df-rex 3065
This theorem is referenced by:  genpass  11003  mulsuniflem  27999  addsdilem2  28002  mulsasslem1  28013  mulsasslem2  28014  dfcgra2  28584  axeuclid  28724  wspthsnwspthsnon  29674  dya2iocnrect  33809  satfv0  34876  satfv1  34881  satf0  34890  itg2addnclem3  37053  prprelprb  46739  prprspr2  46740
  Copyright terms: Public domain W3C validator