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

Theorem rexbii2 3211
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 1833 . 2 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3113 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3113 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 304 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  wex 1765  wcel 2083  wrex 3108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795
This theorem depends on definitions:  df-bi 208  df-ex 1766  df-rex 3113
This theorem is referenced by:  rexbiia  3212  rexbii  3213  rexeqbii  3289  rexrab  3628  rexin  4142  rexdifpr  4509  rexdifsn  4640  reusv2lem4  5200  reusv2  5202  wfi  6063  rexuz2  12152  rexrp  12264  rexuz3  14546  infpn2  16082  efgrelexlemb  18607  cmpcov2  21686  cmpfi  21704  txkgen  21948  cubic  25112  sumdmdii  29879  bnj882  31810  bnj893  31812  frpoind  32691  frind  32696  madeval2  32901  heibor1  34641  eldmqsres  35096  prtlem100  35547  islmodfg  39175  limcrecl  41473
  Copyright terms: Public domain W3C validator