Metamath Proof Explorer


Theorem reubii

Description: Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 22-Oct-1999)

Ref Expression
Hypothesis reubii.1
|- ( ph <-> ps )
Assertion reubii
|- ( E! x e. A ph <-> E! x e. A ps )

Proof

Step Hyp Ref Expression
1 reubii.1
 |-  ( ph <-> ps )
2 1 a1i
 |-  ( x e. A -> ( ph <-> ps ) )
3 2 reubiia
 |-  ( E! x e. A ph <-> E! x e. A ps )