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

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

Proof of Theorem 2rexbii
StepHypRef Expression
1 2rexbii.1 . . 3 (𝜑𝜓)
21rexbii 3094 . 2 (∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 𝜓)
32rexbii 3094 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071
This theorem is referenced by:  rexnal3  3136  3reeanv  3230  2nreu  4444  poxp2  8168  poxp3  8175  poseq  8183  1sdom  9284  ttrcltr  9756  addcompr  11061  mulcompr  11063  4fvwrd4  13688  ntrivcvgmul  15938  prodmo  15972  pythagtriplem2  16855  pythagtrip  16872  cat1  18142  isnsgrp  18736  efgrelexlemb  19768  ordthaus  23392  regr1lem2  23748  fmucndlem  24300  madeval2  27892  zaddscl  28380  zmulscld  28383  dfcgra2  28838  axpasch  28956  axeuclid  28978  axcontlem4  28982  umgr2edg1  29228  wwlksnwwlksnon  29935  xrofsup  32771  satfvsucsuc  35370  satf0  35377  altopelaltxp  35977  brsegle  36109  fimgmcyclem  42543  fimgmcyc  42544  mzpcompact2lem  42762  sbc4rex  42800  7rexfrabdioph  42811  expdiophlem1  43033  fourierdlem42  46164  prpair  47488  ldepslinc  48426  sepnsepolem1  48819
  Copyright terms: Public domain W3C validator