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

Theorem rexbii2 3068
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 1814 . 2 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥(𝑥𝐵𝜓))
3 df-rex 2947 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 2947 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 292 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wex 1744  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-ex 1745  df-rex 2947
This theorem is referenced by:  rexbiia  3069  rexbii  3070  rexeqbii  3083  rexrab  3403  rexdifpr  4238  rexdifsn  4356  reusv2lem4  4902  reusv2  4904  wefrc  5137  wfi  5751  bnd2  8794  rexuz2  11777  rexrp  11891  rexuz3  14132  infpn2  15664  efgrelexlemb  18209  cmpcov2  21241  cmpfi  21259  subislly  21332  txkgen  21503  cubic  24621  sumdmdii  29402  pcmplfin  30055  bnj882  31122  bnj893  31124  imaindm  31806  frpoind  31865  frind  31868  madeval2  32061  heibor1  33739  eldmqsres  34192  prtlem100  34463  islmodfg  37956  limcrecl  40179
  Copyright terms: Public domain W3C validator