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

Theorem rexbii2 3108
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 1871 . 2 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3090 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3090 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 306 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 400  wex 1802  wcel 2145  wrex 3089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832
This theorem depends on definitions:  df-bi 210  df-ex 1803  df-rex 3090
This theorem is referenced by:  rexbiia  3110  rexeqbii  3338  rexrab  3662  rexin  4205  rexdifpr  4621  rexdifsn  4757  reusv2lem4  5363  reusv2  5365  frpoind  6333  eldifsucnn  8638  frind  9710  rexuz2  12914  rexrp  13030  rexuz3  15390  infpn2  16963  efgrelexlemb  19811  cmpcov2  23508  cmpfi  23526  txkgen  23770  cubic  26972  madeval2  27984  sumdmdii  32676  extdgfialglem1  33999  bnj882  35231  bnj893  35233  heibor1  38321  eldmqsres  38804  prtlem100  39495  islmodfg  43658  iuneq1i  45662  limcrecl  46203
  Copyright terms: Public domain W3C validator