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

Theorem rexbii2 3238
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 1933 . 2 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3113 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3113 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43bitr4i 294 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  wex 1859  wcel 2157  wrex 3108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894
This theorem depends on definitions:  df-bi 198  df-ex 1860  df-rex 3113
This theorem is referenced by:  rexbiia  3239  rexbii  3240  rexeqbii  3253  rexrab  3577  rexin  4051  rexdifpr  4410  rexdifsn  4526  reusv2lem4  5081  reusv2  5083  wefrc  5316  wfi  5937  bnd2  9010  rexuz2  11964  rexrp  12074  rexuz3  14318  infpn2  15841  efgrelexlemb  18371  cmpcov2  21415  cmpfi  21433  subislly  21506  txkgen  21677  cubic  24800  sumdmdii  29612  pcmplfin  30262  bnj882  31328  bnj893  31330  imaindm  32011  frpoind  32070  frind  32073  madeval2  32266  heibor1  33926  eldmqsres  34374  prtlem100  34644  islmodfg  38145  limcrecl  40346
  Copyright terms: Public domain W3C validator