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

Theorem rexbii2 3088
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 1845 . 2 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3069 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3069 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 303 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wex 1776  wcel 2106  wrex 3068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-ex 1777  df-rex 3069
This theorem is referenced by:  rexbiia  3090  rexeqbii  3343  rexrab  3705  rexin  4256  rexdifpr  4664  rexdifsn  4799  reusv2lem4  5407  reusv2  5409  frpoind  6365  wfiOLD  6374  eldifsucnn  8701  frind  9788  rexuz2  12939  rexrp  13054  rexuz3  15384  infpn2  16947  efgrelexlemb  19783  cmpcov2  23414  cmpfi  23432  txkgen  23676  cubic  26907  madeval2  27907  sumdmdii  32444  bnj882  34919  bnj893  34921  heibor1  37797  eldmqsres  38269  prtlem100  38841  islmodfg  43058  iuneq1i  45025  limcrecl  45585
  Copyright terms: Public domain W3C validator