Theorem rexbiia 2958

Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)

Hypothesis

Ref	Expression
rexbiia.1

Assertion

Ref	Expression
rexbiia

Proof of Theorem rexbiia

Step	Hyp	Ref	Expression
1		rexbiia.1	. . 3
2	1	pm5.32i 637	. 2
3	2	rexbii2 2957	1

Syntax hints:  ->wi 4  <->wb 184  e.wcel 1818  E.wrex 2808

This theorem is referenced by:  2rexbiia  2973  ceqsrexbv  3234  reu8  3295  f1oweALT  6784  reldm  6851  seqomlem2  7135  fofinf1o  7821  wdom2d  8027  unbndrank  8281  cfsmolem  8671  fin1a2lem5  8805  fin1a2lem6  8806  infm3  10527  wwlktovfo  12896  znf1o  18590  lmres  19801  ist1-2  19848  itg2monolem1  22157  lhop1lem  22414  elaa  22712  ulmcau  22790  reeff1o  22842  recosf1o  22922  chpo1ubb  23666  istrkg2ld  23858  wlknwwlknsur  24712  wlkiswwlksur  24719  wwlkextsur  24731  nmopnegi  26884  nmop0  26905  nmfn0  26906  adjbd1o  27004  atom1d  27272  abfmpunirn  27490  rearchi  27832  eulerpartgbij  28311  eulerpartlemgh  28317  subfacp1lem3  28626  dfrdg2  29228  heiborlem7  30313  eq0rabdioph  30710  fourierdlem70  31959  fourierdlem80  31969  rexrsb  32174

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-an 371  df-ex 1613  df-rex 2813