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

Theorem rexbii2 2957
 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 1667 . 2
3 df-rex 2813 . 2
4 df-rex 2813 . 2
52, 3, 43bitr4i 277 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  /\wa 369  E.wex 1612  e.wcel 1818  E.wrex 2808 This theorem is referenced by:  rexbiia  2958  rexbii  2959  rexeqbii  2972  rexrab  3263  rexdifsn  4159  reusv2lem4  4656  reusv2  4658  wefrc  4878  bnd2  8332  rexuz2  11161  rexrp  11268  rexuz3  13181  infpn2  14431  efgrelexlemb  16768  cmpcov2  19890  cmpfi  19908  subislly  19982  txkgen  20153  cubic  23180  sumdmdii  27334  pcmplfin  27863  wfi  29287  frind  29323  heibor1  30306  prtlem100  30596  islmodfg  31015  limcrecl  31635  rexdifpr  32300  bnj882  33984  bnj893  33986 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631 This theorem depends on definitions:  df-bi 185  df-ex 1613  df-rex 2813
 Copyright terms: Public domain W3C validator