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

Theorem rexbii2 3032
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 1771 . 2 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥(𝑥𝐵𝜓))
3 df-rex 2913 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 2913 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 292 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wex 1701  wcel 1987  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-rex 2913
This theorem is referenced by:  rexbiia  3033  rexbii  3034  rexeqbii  3047  rexrab  3352  rexdifpr  4176  rexdifsn  4292  reusv2lem4  4832  reusv2  4834  wefrc  5068  wfi  5672  bnd2  8700  rexuz2  11683  rexrp  11797  rexuz3  14022  infpn2  15541  efgrelexlemb  18084  cmpcov2  21103  cmpfi  21121  subislly  21194  txkgen  21365  cubic  24476  sumdmdii  29123  pcmplfin  29709  bnj882  30704  bnj893  30706  frind  31441  heibor1  33241  prtlem100  33623  islmodfg  37119  limcrecl  39265
  Copyright terms: Public domain W3C validator