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

Theorem rexbii2 3090
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 1851 . 2 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3071 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3071 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 303 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wex 1782  wcel 2107  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-rex 3071
This theorem is referenced by:  rexbiia  3092  rexeqbii  3315  rexrab  3655  rexin  4200  rexdifpr  4620  rexdifsn  4755  reusv2lem4  5357  reusv2  5359  frpoind  6297  wfiOLD  6306  eldifsucnn  8611  frind  9691  rexuz2  12829  rexrp  12941  rexuz3  15239  infpn2  16790  efgrelexlemb  19537  cmpcov2  22757  cmpfi  22775  txkgen  23019  cubic  26215  madeval2  27205  sumdmdii  31399  bnj882  33595  bnj893  33597  heibor1  36315  eldmqsres  36793  prtlem100  37367  islmodfg  41439  limcrecl  43956
  Copyright terms: Public domain W3C validator