Theorem rexbiia 2134

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

Syntax hints:   -> wi 3   <-> wb 163   e. wcel 1300  E.wrex 2106

This theorem is referenced by:  2rexbiia 2135  reu8 2448  f1oweALT 4883  unbndrank 5794  infm3 7263  reeff1o 8691  efghgrpilem 10073  efifo 10083  projlemHIL 10851  pjpj0i 10888  nmopnegi 11526  nmop0 11547  nmfn0 11548  adjbd1o 11655  atom1d 11925  prsubrtr 14763  caures 15852

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-rex 2110

Copyright terms: Public domain