Theorem rexbiia 1674

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 645	. 2 |- ((x e. A /\ ph) <-> (x e. A /\ ps))
3	2	rexbii2 1672	1 |- (E.x e. A ph <-> E.x e. A ps)

Syntax hints:   -> wi 3   <-> wb 146   e. wcel 958  E.wrex 1646

This theorem is referenced by:  2rexbiia 1675  reu8 1936  f1oweALT 3906  unbndrank 4683  infm3 6054  reeff1o 7426  efghgrpilem 8719  efifo 8729  projlemHIL 9218  pjpj0 9255  nmopneg 9889  nmop0 9910  nmfn0 9911  adjbd1o 10018  atom1d 10280

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-rex 1650

Copyright terms: Public domain