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

Theorem rexbii2 3082
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 1842 . 2 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3063 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3063 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 303 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 395  wex 1773  wcel 2098  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 206  df-ex 1774  df-rex 3063
This theorem is referenced by:  rexbiia  3084  rexeqbii  3331  rexrab  3684  rexin  4231  rexdifpr  4653  rexdifsn  4789  reusv2lem4  5389  reusv2  5391  frpoind  6333  wfiOLD  6342  eldifsucnn  8658  frind  9740  rexuz2  12879  rexrp  12991  rexuz3  15291  infpn2  16842  efgrelexlemb  19655  cmpcov2  23204  cmpfi  23222  txkgen  23466  cubic  26685  madeval2  27684  sumdmdii  32092  bnj882  34392  bnj893  34394  heibor1  37134  eldmqsres  37611  prtlem100  38185  islmodfg  42266  limcrecl  44796
  Copyright terms: Public domain W3C validator