Theorem rexbiia 1666

Description: Inference adding restricted existential quantifier to both sides of an equivalence.

Hypothesis

Ref	Expression
ralbiia.1	|- (x e. A -> (ph <-> ps))

Assertion

Ref	Expression
rexbiia	|- (E.x e. A ph <-> E.x e. A ps)

Proof of Theorem rexbiia

Step	Hyp	Ref	Expression
1		ralbiia.1	. . 3 |- (x e. A -> (ph <-> ps))
2	1	pm5.32i 643	. 2 |- ((x e. A /\ ph) <-> (x e. A /\ ps))
3	2	rexbii2 1664	1 |- (E.x e. A ph <-> E.x e. A ps)

Syntax hints:   -> wi 3   <-> wb 146   e. wcel 955  E.wrex 1638

This theorem is referenced by:  2rexbiia 1667  reu8 1926  f1oweALT 3891  unbndrank 4655  infm3 6001  reeff1o 7368  efghgrpilem 8634  efifo 8644  pjpj0 9170  nmopneg 9805  nmop0 9826  nmfn0 9827  adjbd1o 9933  atom1d 10188

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-rex 1642

Copyright terms: Public domain