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

Theorem 2rexbii 3189
Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
Hypothesis
Ref Expression
rexbii.1 (𝜑𝜓)
Assertion
Ref Expression
2rexbii (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜓)

Proof of Theorem 2rexbii
StepHypRef Expression
1 rexbii.1 . . 3 (𝜑𝜓)
21rexbii 3188 . 2 (∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 𝜓)
32rexbii 3188 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 198  wrex 3083
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-rex 3088
This theorem is referenced by:  rexnal3  3199  ralnex2OLD  3201  ralnex3OLD  3203  3reeanv  3303  2nreu  4270  addcompr  10233  mulcompr  10235  4fvwrd4  12836  ntrivcvgmul  15108  prodmo  15140  pythagtriplem2  16000  pythagtrip  16017  isnsgrp  17746  efgrelexlemb  18626  ordthaus  21686  regr1lem2  22042  fmucndlem  22593  dfcgra2  26308  axpasch  26420  axeuclid  26442  axcontlem4  26446  umgr2edg1  26686  wwlksnwwlksnon  27411  xrofsup  30233  poseq  32556  madeval2  32751  altopelaltxp  32898  brsegle  33030  mzpcompact2lem  38688  sbc4rex  38727  7rexfrabdioph  38738  expdiophlem1  38959  fourierdlem42  41811  prpair  42971  ldepslinc  43871
  Copyright terms: Public domain W3C validator