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

Theorem rexbii2 3021
 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 1764 . 2 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥(𝑥𝐵𝜓))
3 df-rex 2902 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 2902 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 291 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-ex 1696  df-rex 2902 This theorem is referenced by:  rexbiia  3022  rexbii  3023  rexeqbii  3036  rexrab  3337  rexdifsn  4264  reusv2lem4  4798  reusv2  4800  wefrc  5032  wfi  5630  bnd2  8639  rexuz2  11615  rexrp  11729  rexuz3  13936  infpn2  15455  efgrelexlemb  17986  cmpcov2  21003  cmpfi  21021  subislly  21094  txkgen  21265  cubic  24376  sumdmdii  28658  pcmplfin  29255  bnj882  30250  bnj893  30252  frind  30984  heibor1  32779  prtlem100  33161  islmodfg  36657  limcrecl  38696  rexdifpr  40315
 Copyright terms: Public domain W3C validator