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

Theorem rexbii2 3177
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 1923 . 2 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3056 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3056 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 292 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wex 1853  wcel 2139  wrex 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-ex 1854  df-rex 3056
This theorem is referenced by:  rexbiia  3178  rexbii  3179  rexeqbii  3192  rexrab  3511  rexdifpr  4350  rexdifsn  4469  reusv2lem4  5021  reusv2  5023  wefrc  5260  wfi  5874  bnd2  8929  rexuz2  11932  rexrp  12046  rexuz3  14287  infpn2  15819  efgrelexlemb  18363  cmpcov2  21395  cmpfi  21413  subislly  21486  txkgen  21657  cubic  24775  sumdmdii  29583  pcmplfin  30236  bnj882  31303  bnj893  31305  imaindm  31987  frpoind  32046  frind  32049  madeval2  32242  heibor1  33922  eldmqsres  34375  prtlem100  34648  islmodfg  38141  limcrecl  40364
  Copyright terms: Public domain W3C validator