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

Theorem rexbii2 3174
 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 1850 . 2 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3077 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3077 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 307 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1782   ∈ wcel 2112  ∃wrex 3072 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812 This theorem depends on definitions:  df-bi 210  df-ex 1783  df-rex 3077 This theorem is referenced by:  rexbiia  3175  rexeqbii  3251  rexrab  3611  rexin  4145  rexdifpr  4553  rexdifsn  4682  reusv2lem4  5268  reusv2  5270  wfi  6157  rexuz2  12329  rexrp  12441  rexuz3  14746  infpn2  16294  efgrelexlemb  18933  cmpcov2  22080  cmpfi  22098  txkgen  22342  cubic  25524  sumdmdii  30287  bnj882  32416  bnj893  32418  frpoind  33317  frind  33325  madeval2  33587  heibor1  35518  eldmqsres  35973  prtlem100  36425  islmodfg  40376  limcrecl  42627
 Copyright terms: Public domain W3C validator