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

Theorem rexbii2 3089
Description: Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)
Hypothesis
Ref Expression
rexbii2.1 ((𝑥𝐴𝜑) ↔ (𝑥𝐵𝜓))
Assertion
Ref Expression
rexbii2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓)

Proof of Theorem rexbii2
StepHypRef Expression
1 rexbii2.1 . . 3 ((𝑥𝐴𝜑) ↔ (𝑥𝐵𝜓))
21exbii 1847 . 2 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3070 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3070 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 303 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wex 1778  wcel 2107  wrex 3069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808
This theorem depends on definitions:  df-bi 207  df-ex 1779  df-rex 3070
This theorem is referenced by:  rexbiia  3091  rexeqbii  3344  rexrab  3701  rexin  4249  rexdifpr  4658  rexdifsn  4793  reusv2lem4  5400  reusv2  5402  frpoind  6362  wfiOLD  6371  eldifsucnn  8703  frind  9791  rexuz2  12942  rexrp  13057  rexuz3  15388  infpn2  16952  efgrelexlemb  19769  cmpcov2  23399  cmpfi  23417  txkgen  23661  cubic  26893  madeval2  27893  sumdmdii  32435  bnj882  34941  bnj893  34943  heibor1  37818  eldmqsres  38289  prtlem100  38861  islmodfg  43086  iuneq1i  45095  limcrecl  45649
  Copyright terms: Public domain W3C validator